3 ms·
Interactive Theorem Provers are getting productive enough to be useful for real projects. The CompCert project was a real eye opener/motivator for people who wa
by deterministic 5y ago
Interactive Theorem Provers are getting productive enough to be useful for real projects. The CompCert project was a real eye opener/motivator for people who want to develop proven correct software.