Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: anton@mips.complang.tuwien.ac.at (Anton Ertl) Newsgroups: comp.compilers Subject: Re: Are there different programming languages that are compiled to the same intermediate language? Date: Sun, 05 Feb 2023 17:59:03 GMT Organization: Institut fuer Computersprachen, Technische Universitaet Wien Sender: johnl@iecc.com Approved: comp.compilers@iecc.com Message-ID: <23-02-020@comp.compilers> References: <23-02-005@comp.compilers> Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="24730"; mail-complaints-to="abuse@iecc.com" Keywords: theory Posted-Date: 05 Feb 2023 13:44:11 EST X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com Xref: csiph.com comp.compilers:3366 Martin Ward 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/