Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: arnold@skeeve.com (Aharon Robbins) Newsgroups: comp.compilers Subject: Re: Are there different programming languages that are compiled to the same intermediate language? Date: 03 Feb 2023 08:26:45 GMT Organization: SunSITE.dk - Supporting Open source Sender: johnl@iecc.com Approved: comp.compilers@iecc.com Message-ID: <23-02-009@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="97569"; mail-complaints-to="abuse@iecc.com" Keywords: theory Posted-Date: 03 Feb 2023 13:14:28 EST X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com Originator: arnold@skeeve.com (Aharon Robbins) Xref: csiph.com comp.compilers:3359 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 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