4 ms·
> The inductive invariant IC3PO produced for Paxos in under an hour identically matches the human-written one previously derived with significant manual effort
by meetups323 5y ago
> The inductive invariant IC3PO produced for Paxos in under an hour identically matches the human-written one previously derived with significant manual effort using a technique called interactive theorem proving. On top of speeding the process up, it also produces a proof with very succinct and digestible documentation.
Is there anything actually different between "interactive theorem proving" in a sufficiently advanced language (say Coq) and what they've done here? Honest question, I had to drop out of my college Coq class on account of a broken leg (and lack of willpower).
- johnbender 5y agoIn Coq the user generally writes meta programs to generate proofs as programs at varying levels of automation (Ltac scripts). Here they used IC3 to automatically produce proof that their state based model of paxos satisfies the invariant. In principle one could build an automated proof system for a state machine-esque formalism written in Coq using Ltac but that would be a nightmare in practice.