Prove the correctness of a compiler front-end

Path	csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end
From	Roger L Costello <costello@mitre.org>
Newsgroups	comp.compilers
Subject	Prove the correctness of a compiler front-end
Date	Fri, 3 Feb 2023 12:39:28 +0000
Organization	Compilers Central
Sender	johnl@iecc.com
Approved	comp.compilers@iecc.com
Message-ID	<23-02-012@comp.compilers> (permalink)
MIME-Version	1.0
Content-Type	text/plain; charset="us-ascii"
Content-Transfer-Encoding	8bit
Injection-Info	gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="98697"; mail-complaints-to="abuse@iecc.com"
Keywords	theory
Posted-Date	03 Feb 2023 13:17:37 EST
X-submission-address	compilers@iecc.com
X-moderator-address	compilers-request@iecc.com
X-FAQ-and-archives	http://compilers.iecc.com
Thread-Topic	Prove the correctness of a compiler front-end
Thread-Index	Adk3zHR9VAlP53e6SACkLp7EUORYEA==
Accept-Language	en-US
Content-Language	en-US
authentication-results	dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=mitre.org;
X-OriginatorOrg	mitre.org
Xref	csiph.com comp.compilers:3361

Show key headers only | View raw

Fascinating discussion! A summary of the discussion:

Scenario: Prove that the compiler front-end program you just wrote is
correct.

Approach: Use a theorem prover to prove the correctness of the program.

Aharon Robbins: Isn't there a chicken and egg problem? How do we know that the
theorem prover is correct and bug free?

Martin Ward: 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.

Alan Perlis: I don't see any reason to believe that a thousand line proof is
any more likely to be bug-free than a thousand line program.

Martin Ward: 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, nevertheless, the case.

John Levine: 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 programs, the
longer and more complicated they are, the more likely they are to have bugs.

Back to comp.compilers | Previous | Next | Find similar

Thread

Prove the correctness of a compiler front-end Roger L Costello <costello@mitre.org> - 2023-02-03 12:39 +0000

csiph-web