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

Martin Ward <mwardgkc@gmail.com> writes:
>On 01/02/2023 08:07, Aharon Robbins wrote:> I've never understood this.
>> [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]
>
>Mathematicians publish proofs all the time and only a tiny percentage
>of published proofs turn out to have errors.


Even at face value I would like to see some evidence for this claim.


A comparable statement would be "Computer scientists publish papers
about programs all the time, and only a tiny percentage of these
papers turn out to have errors".


There is a difference between how a mathematical proof is used and how
a program is used.


1) A program is usually fed to a machine for execution. A published
proof is read by a number (>=0) of mathematicians, who fill in a lot
of what the author has left out. If you feed the published proof to
an automatic proof checker (of your choice), how many of the published
proofs need no additions and no changes (bug fixes) before the proof
checker verifies the proof. I guess there is a reason why Wikipedia
has no page on "proof checker", but suggests "proof assistant": "a
software tool to assist with the development of formal proofs by
human-machine collaboration."


2) A program has to satisfy the requirements of its users, while a
published proof is limited to proving a published theorem. One
example of the difference is that undefinedness is totally acceptable
in mathematics, while it is a bug in programs (interestingly, there is
a significant number of compiler writers who take the mathematical
view in what they provide to programmers, but consider that a program
in their programming language that exercises the undefined behaviour
that they provide to programmers to be buggy).


The size argument that our esteemed moderator provided also has to be
considered.


- anton
--
M. Anton Ertl
anton@mips.complang.tuwien.ac.at
http://www.complang.tuwien.ac.at/anton/

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