Trust and verification

We talked today about some topics in trust and verification. The mockup Lean 4 code for a verified (very simple!) compiler can be found here. CompCert is a full scale academic/industrial project to do the same for a C compiler.

See the lecture capture for more details.

Last year, Komron Aripov took this idea much farther for his final project in Formal Proof and Verification. His code is here if you're interested in taking a look!