Re: computer language used to program Mars Lander

["John Thingstad" <jpthing@online.no>]

Pￜ Thu, 24 Jul 2008 08:59:11 +0200, skrev jhc0033@gmail.com  
<jhc0033@gmail.com>:

> On Jul 23, 7:43 am, Michael Oswald <muell...@gmx.net> wrote:
>> I mean, I work in the space
>> business (although not directly on on-board software but rather mission
>> control software and testing equipment) but I haven't heard of Lisp
>> usage. Would definitely be a 'nice to know' for me.
>
> Probably because they weren't too successful. I personally think Lisp
> is super-cool, but inappropriate for space (or any reliability-
> sensitive work).
>
> If I remember correctly, when they used Lisp in the probe, there was a
> bug and they used Lisp's live patching and interactive debugging to
> fix it, so they only missed their target by a quadrillion miles
> instead of missing it by a gazillion miles.
>
> On the other hand, the bug wouldn't have happened in the first place,
> if they used a good static language. I'll let someone who knows better
> fill in the details (that's why I added comp.lang.lisp to the groups)
>
> Happy space exploration and exploitation!

Mathematically verify it with ACL2! Way better than silly type checking.
Check that theprogram does what the spec sais.
(Which still only proves that it does what you say, not what you men.))

--------------
John Thingstad