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

[Michael Schuerig]

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