Path: csiph.com!1.us.feeder.erje.net!3.us.feeder.erje.net!feeder.erje.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: Martin Ward Newsgroups: comp.compilers Subject: Re: Are there different programming languages that are compiled to the same intermediate language? Date: Thu, 2 Feb 2023 15:44:17 +0000 Organization: Compilers Central Sender: johnl@iecc.com Approved: comp.compilers@iecc.com Message-ID: <23-02-005@comp.compilers> Reply-To: martin@gkc.org.uk MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="69848"; mail-complaints-to="abuse@iecc.com" Keywords: theory, comment Posted-Date: 02 Feb 2023 20:05:59 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:3357 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. > [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. 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. -- Martin Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4 [Computer programs tend to be a lot longer than mathematical proofs. I realize there are some 500 page proofs, but there are a whole lot of 500 page programs. It is my impression that in proofs, as in progams, the longer and more complicated they are, the more likely they are to have bugs. -John]