Re: Are there different programming languages that are compiled to the same intermediate language?

Dr. Ward replied to me privately also, but since this went to the group,
I'll say the same thing here that I replied to him.


In article 23-02-005, Martin Ward <martin@gkc.org.uk> wrote:
>On 01/02/2023 08:07, Aharon Robbins wrote:
>> I've never understood this. Isn't there a chicken and egg problem?
>> How do we know that the theorem prover is correct and bug free?


>A theorem prover generates a proof of the theorem (if it succeeds).
>Checking the correctness of a proof is a much simpler task
>than finding the proof in the first place and can be carried
>out independently by different teams using different methods.
>Appel and Haken's proof of the four colour theorem, for example,
>involved a significant element of computer checking which was
>independently double checked with different programs and computers.


This tells me what a theorem prover does, and why it's useful. It
does not answer my question: How do we know that the theorem prover
itself is correct and bug free?


>> [It's a perfectly reasonable question. Alan Perlis, who was my thesis
>> advisor, never saw any reason to believe that a thousand line proof
>> was any more likely to be bug-free than a thousand line program.
>> -John]


And this is a different point from my question.


>Mathematicians publish proofs all the time and only a tiny percentage
>of published proofs turn out to have errors. Programmers release
>programs all the time and a vanishingly small percentage of these
>turn out to be free from all bugs. Alan Perlis may not have been able
>to think of a reason why this should be the case, but it is,
>nevetheless, the case.


I don't argue this. But I think mathematical theorems and their
proofs are different qualitatively from real world large programs.
I do think there's room for mathematical techniques to help
improve software development, but I don't see that done down
in the trenches, and I've been down in the trenches for close
to 40 years.


Arnold
--
Aharon (Arnold) Robbins arnold AT skeeve DOT com

Return to the comp.compilers page.
Search the comp.compilers archives again.