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

[Heinrich Apfelmus]

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