3 ms·
Nope. CompCert is an example of a small team of people writing a proven correct C compiler. seL4 is another. The problem is training. Universities are currently
by deterministic 3y ago
Nope. CompCert is an example of a small team of people writing a proven correct C compiler. seL4 is another. The problem is training. Universities are currently not training CS students to prove code correct. This will change. But slowly.