This is an automated archive made by the Lemmit Bot.

The original was posted on /r/programminglanguages by /u/FurCollarCriminal on 2024-04-04 22:51:36.

Compilers seem like a good use-case for formal verification at first glance: they’re complex deterministic programs where correctness is of the utmost importance.

While there is the canonical example of the “verified C compiler” I don’t really understand how formal verification fits into the compiler world at large.

Has anyone here applied formal verification to their work? Perhaps for one part of their compiler – verifying the type checker, a specific optimization, etc? What did it look like? What tools did you use?