On Tuesday 08 June 2010, Heinrich Apfelmus wrote:
Michael Schuerig wrote:
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 absolutely no experience with real time system, but if I were tasked to write with these coding standards, I would refuse and instead create a small DSL in Haskell that compiles to the requested subset of C.
That suggestion is similar to the approach taken by "verifiable" languages, as Matthias describes it in a parallel reply. Now, the interesting question is, whether it is possible to define a DSL that's expressive enough and still can be translated to a very restrictive subset of C. I wouldn't expect the on-board functionality of a space probe or rover to be trivial. I think it would count as cheating if you compile down a DSL to C code that only takes a fixed chunk of memory, but then itself manages blocks of that memory dynamically.
After all, the question is this: why use C if you don't actually use C? The reason is probably that designing/writing a proper DSL is considered too error prone, but with today's theorem provers, this should no longer be the case.
As I understood Holzmann in his talk, use of C is a kind of cultural heritage at JPL. BTW, thanks for your recent video on GADTs. Michael -- Michael Schuerig mailto:michael@schuerig.de http://www.schuerig.de/michael/