Re: computer language used to program Mars Lander

["Brian" <phaedrusalt@hotmail.com>]

<jhc0033@gmail.com> wrote in message 
news:6e2a8ce8-25e9-427b-9c67-3285ce73e398@j7g2000prm.googlegroups.com...
> On Jul 24, 1:39 pm, "Brian" <phaedrus...@hotmail.com> wrote:
>> <jhc0...@gmail.com> wrote in message
>>
>> news:76fc184b-bd62-4bd3-9ccf-8a6cd872c30b@v39g2000pro.googlegroups.com...
>>
>> > On Jul 24, 12:39 am, "John Thingstad" <jpth...@online.no> 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*
>
> I think "Coq" conveys a feeling of confidence that a theorem prover
> should. (Btw thanks for ruining the discussion with your low-brow
> shtik)

After the ACL2 comment, it seemed appropriate.  I doubt if one comment 
"ruined" the discussion for anyone.  Well, anyone other than those whose 
craniums are firmly emplaced in their anal orifice...  (High-brow shtik is 
sooo much better!)

Really, I find it's usually those who make tone, content or format comments 
that tend to bring down the discussion.  A little levity rarely hurts much, 
and I'm sure you'll get over it.

And btw, you're welcome.