[Haskell-cafe] Stone age programming for space age hardware?

[Michael Schuerig]

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:michael at schuerig.de
http://www.schuerig.de/michael/