4 ms·
Do Amazon actually write their own HOL-based prover from scratch?
by auggierose 2y ago
Do Amazon actually write their own HOL-based prover from scratch?
- GregarianChild 2y agoI don't know, but given that AWS has 1000s if note millions of servers that may have idle cycles, it makes sense to use them for automatic theorem proving. And there is no existing ITP or even SMT solver that was specifically designed for efficient use of so much parallelism. AWS certainly hired a lot of senior STM and ITP guys, such as John Harrison.