Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.compilers > #3359

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

Show key headers only | View raw

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@comp.compilers>, 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

Back to comp.compilers | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Re: Are there different programming languages that are compiled to the same intermediate language? Martin Ward <mwardgkc@gmail.com> - 2023-02-02 15:44 +0000
  Re: Are there different programming languages that are compiled to the same intermediate language? arnold@skeeve.com (Aharon Robbins) - 2023-02-03 08:26 +0000
  Re: Are there different programming languages that are compiled to the same intermediate language? anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2023-02-05 17:59 +0000
    Re: Proofs, was Are there different programming languages that are compiled to the same intermediate language? Spiros Bousbouras <spibou@gmail.com> - 2023-02-05 19:23 +0000

csiph-web