Michael Schuerig wrote:
Heinrich Apfelmus wrote:
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.
Ah, I had in mind that the embedded DSL represents the target subset of C verbatim, very much in the spirit of Lennart Augustsson's reimplementation of BASIC http://tinyurl.com/augustss-BASIC http://hackage.haskell.org/cgi-bin/hackage-scripts/package/BASIC In other words, I'm thinking of a direct copy of the target language in Haskell. This way, you can use the type system to reject programs that don't adhere to the coding standards, which would be the main point of this embedding. But you get a huge benefit on top of that: Haskell now serves as a macro language and you can implement many abstractions that are not directly available in the target language, like custom control structures ("foreach") or exceptions (to organize these abundant checks for error conditions). Of course, the main goal of the NASA restrictions is to make the code so simple that it has no obvious deficiencies, but what better way is there to do that than finding and expressing - even small-scale - abstractions? (The foreach statement seems to be a convincing example.)
As I understood Holzmann in his talk, use of C is a kind of cultural heritage at JPL.
Ah well, the shackles of habit... In the matter of program design, I am unconvinced of any cultural heritage that is not based on the mathematical clarity of Edsger W. Dijkstra. ;)
BTW, thanks for your recent video on GADTs.
My pleasure. :) I'm already planning another video experiment. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com