Re: computer language used to program Mars Lander

<jhc0033@[EMAIL PROTECTED]
> wrote in message 
news:76fc184b-bd62-4bd3-9ccf-8a6cd872c30b@[EMAIL PROTECTED]
> On Jul 24, 12:39 am, "John Thingstad" <jpth...@[EMAIL PROTECTED]
> wrote:
>
>> 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.))
>>
>
> Typo-prone people probably shouldn't use dynamically-typed languages!
> BTW us, static folk, got Coq, which is probably better than ACL2: the
> name "ACL2" sounds like they couldn't even get it right in the first
> try.

You've "got Coq"???  And you're willing to talk about bad names?
*grin*