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

[Hans van Thiel]

That's interesting, writing a DSL that compiles to C. I've actually
inerviewed Gerard Holzamann twice, the first time when he received the
ACM Software System Award in 2002 [1] and in 2008 after he moved to JPL
[2]. What they use to test distributed software is the Process Meta
Language (Promela) which models communication between distributed
processes. Now Spin checks all possible models for deadlock, liveness
etc. You can also use asserts to test conditions, just as in C. 
It also uses LTL (linear temporal logic) to formulate statements like,
"will the railroad crossing always eventually open" and such. Two
articles about Spin are [3] and [4]. Unfortunately, all four are in
Dutch, but, hey, surely somebody here must  be able to read that
language <g>. The articles on Spin contain listings in Promela.
Now, what Gerard Holzmann told me in the interview, is that NASA is very
conservative in it's use of software tools. They don't use C++, just C,
and a well defined version of the GNU C compiler at that. The coding
standards, which even prohibit the use of C pointers, are aimed to keep
everything as simple as possible. Just imagine hundreds of people
working over many years to produce code where any error, how trivial it
may be, will occur millions of miles away, cost hundreds of millions of
dollars, and could damage the reputation of the company and its future
funding. Now, if you can use a DSL to make embedded software absolutely
failsafe, that would certainly grab NASA's attention. But again, they
are very conservative, it seems...

[1] http://muitovar.com/pub/pdf/holzmann.pdf 
[2] http://muitovar.com/pub/pdf/acmaw.pdf 
[3] http://muitovar.com/pub/pdf/spin1.pdf 
[4] http://muitovar.com/pub/pdf/spin2.pdf 


On Tue, 2010-06-08 at 18:27 +0200, 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.
> 
> 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.
> 
> 
> Regards,
> Heinrich Apfelmus
> 
> --
> http://apfelmus.nfshost.com
> 
>