Re: [Haskell-cafe] Stone age programming for space age hardware?
Hi, The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine. for some safety critical applications that require certification, SCADE with the underlying Lustre language is used. It has formal semantics and some properties can be checked with automatic verification (up to linear arithmetic). The Lustre dataflow programs are then transformed to C (or Ada), by compiling to automata and representing those in C. This transformation is realized in Ocaml afaik. I think these kind of transformations, maybe specifying an embedded DSL instead of using a language like Lustre resulting in C with static bounds etc. could be a way to use Haskell. But anything using dynamic memory allocation, GC etc. is dangerous for real-time bounds. These programs also often run on old outdated, but reliable HW for which mainly C compilers exist. The used standards only allow a certain set of programming languages (or subsets of these languages) and you even have to use proved and tested compilers and tools. I have a hunch that the real restrictions of this kind of software are not concerned with fixed memory, iterations, whatever, but rather with guaranteed bounds. If that is indeed the case, how feasible would it be to prove relevant properties for systems programmed in Haskell? I think proving the correct transformation of some input language to static C using Haskell is possible. Functional languages like Haskell or Ocaml in the case of SCADE are well suited to this, due to lack of loops, side effects etc. I think atom is such a DSL embedded into Haskell that can generate code for real-time systems. regards Matthias ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Stone age programming for space age hardware?
A few days ago, I watched a presentation by Gerard Holzmann on the development methodology and programming techniques used at JPL for writing the software for the next Mars mission. I found the talk entertaining and learned a few things. http://www.infoq.com/presentations/Scrub-Spin Among the arsenal of methods they use to ensure correctness is model checking for the algorithms used as well as rather restrictive coding standards. Well, model checking sounds good, real formal oomph. But the coding itself? For one thing, they're using C. On top of that, the coding standards prohibit dynamic memory allocation, recursion, and loops without explicit bounds; see [*] for more details. I was dumbfounded, although I have known all this. I have no personal experience with either embedded or real time software, but I've been aware that C still is the most popular language for that purpose and that coding standards are very restrictive. The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine. I have a hunch that the real restrictions of this kind of software are not concerned with fixed memory, iterations, whatever, but rather with guaranteed bounds. If that is indeed the case, how feasible would it be to prove relevant properties for systems programmed in Haskell? Michael [*] http://spinroot.com/gerard/pdf/Power_of_Ten.pdf -- Michael Schuerig mailto:mich...@schuerig.de http://www.schuerig.de/michael/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Stone age programming for space age hardware?
On 07/06/2010, at 3:05 AM, Michael Schuerig wrote: I have a hunch that the real restrictions of this kind of software are not concerned with fixed memory, iterations, whatever, but rather with guaranteed bounds. If that is indeed the case, how feasible would it be to prove relevant properties for systems programmed in Haskell? For full Haskell that includes laziness and general recursion: not very. Proving properties about the values returned by functions is one thing, but giving good guaranteed upper bounds to the time and space used by an arbitrary program can be very difficult. See for example: J ̈orgen Gustavsson and David Sands, Possibilities and limitations of call-by-need space improvement, ICFP 2001: Proc. of the International Conference on Functional Programming, ACM, 2001, pp. 265–276. Adam Bakewell and Colin Runciman, A model for comparing the space usage of lazy evaluators, PPDP 2000: Proc. of the International Conference on Principles and Practice of Declarative Pro- gramming, ACM, 2000, pp. 151–162. Hans-Wolfgang Loidl. Granularity in Large-Scale Parallel Functional Programming. PhD Thesis. Department of Computing Science, University of Glasgow, March 1998. I expect future solutions for this domain will look more like the Hume (family of) languages [1]. They give several language levels, and can give stronger bounds for programs using less language features. [1] http://www-fp.cs.st-andrews.ac.uk/hume/index.shtml ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
