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
- What Every C Programmer Should Know About Undefined Behavior #2/3 - The LLVM Project Blogblog.llvm.org
- What Every C Programmer Should Know About Undefined Behavior #3/3 - The LLVM Project Blogblog.llvm.org
- A friendly introduction to machine learning compilers and optimizershuyenchip.com
- A shallow dive into formal verificationvitalik.eth.limo
- Formally speaking, "Transpiler" is a useless word | Rachit Nigampeople.csail.mit.edu
- Why ML/OCaml are good for writing compilersflint.cs.yale.edu
- Against Query Based Compilersmatklad.github.io
- Compilers - What Every Programmer Should Know About Compiler Optimizations | Microsoft Learnlearn.microsoft.com
- What can we learn from how compilers are designed?tedinski.com
- Writing a C compiler in 500 lines of Pythonvgel.me
- A Gentle Introduction to LLVM IR · mcyoungmcyoung.xyz
- Compiler Optimizations Are Hard Because They Forget - Faultlorefaultlore.com