I think there is a project quite similar to this one called Verifiable Software Toolchain (VST) in which you can write a C program, convert it into a massive Co

I think there is a project quite similar to this one called Verifiable Software Toolchain (VST) in which you can write a C program, convert it into a massive Coq expression, and then write theorems about that expression in Coq. The Software Foundations series has a volume about it [1], which I found to be an order of magnitude harder to understand than the other volumes. It feels like the magmide project aims to the same goal as VST. It's unclear how it will improve on what VST has done. It may just be that formal verification of real world languages is inherently complex. [1] https://softwarefoundations.cis.upenn.edu/vc-current/index.html https://softwarefoundations.cis.upenn.edu/vc-current/index.h...