Fri, 3 Feb 2023 12:39:28 +0000

Related articles |
---|

Prove the correctness of a compiler front-end costello@mitre.org (Roger L Costello) (2023-02-03) |

From: | Roger L Costello <costello@mitre.org> |

Newsgroups: | comp.compilers |

Date: | Fri, 3 Feb 2023 12:39:28 +0000 |

Organization: | Compilers Central |

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 |

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 |

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.

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.