from armchair_progamer@programming.dev to programming_languages@programming.dev on 27 Mar 2024 01:29
https://programming.dev/post/11976600
Verified compiler specifically means that, besides the compiler itself, the authors have written an interpreter for the source language (here, PureLang) and target language (assembly). They then proved that, for any valid program P, the observable behavior (like side-effects but not quite) produced by source_interpreter(P) is identical to the observable behavior produced by target_interpreter(compiler(P)).
Note that the source interpreter and compiler can both be buggy. Or compiler and target interpreter, or source and target interpreters, or proof kernel, or language the interpreters are written in, or the CPU itself, or probably other things. See The Trusted Computing Base of the CompCert Verified Compiler.
CompCert was the first large-scale formally-verified compiler, publicly released in 2008 and still being improved today. It compiles C99 to a variety of CPU architectures. More recently, CakeML is a formally-verified compiler for a functional language, specifically a subset of Standard ML. This is harder because ML’s semantics are further from assembly than C’s; for example, the developers of CakeML also had to formally verify a garbage collector. And lastly, PureCake itself is a compiler for an even higher-level language: it similar to Haskell, and like Haskell, everything is lazy and purely functional, and side effects are through monads (example).
Thesis: Verified compilation of a purely functional language to a realistic machine semantics. Part 1 is about PureCake, part 2 is about converting an official ARM assembly specification into the proof language partly automatically (making “the target interpreter is buggy” less likely, although still possible).
threaded - newest