What even is compiler correctness?
In this post I precisely define common compiler correctness properties. Compilers correctness properties are often referred to by vague terms such as "correctness", "compositional correctness", "separate compilation", "secure compilation", and others. I m...
In this post I precisely define common compiler correctness properties. Compilers correctness properties are often referred to by vague terms such as “correctness”, “compositional correctness”, “separate compilation”, “secure compilation”, and others. I make these definitions precise and discuss the key differences. I give examples of research papers and projects that develop compilers that satisfy each of these properties. What is a Language Our goal is to give a generic definition to compiler correctness properties without respect to a particular compiler, language, or class of languages. We
saved by
related reading
- The LLVM Compiler Infrastructure Projectllvm.org
- Formally speaking, "Transpiler" is a useless word | Rachit Nigampeople.csail.mit.edu
- Thompson_1984_ReflectionsonTrustingTrust.pdfcs.cmu.edu
- Claude Is Not a Compilerblog.exe.dev
- Why ML/OCaml are good for writing compilersflint.cs.yale.edu
- rsc-phd-thesis.pdfpdos.csail.mit.edu
- Rambles around computer sciencehumprog.org
- Google's Fully Homomorphic Encryption Compiler — A Primer || Math ∩ Programmingjeremykun.com
- How Compiler Explorer Works in 2025 — Matt Godbolt’s blogxania.org
- [2011.07966] A Modern Compiler for the French Tax Codearxiv.org
- Against Query Based Compilersmatklad.github.io
- Type system - Wikipediaen.wikipedia.org