3 ms·
>> I've had to write short inductive proofs in several of the systems I've built. In what context was this necessary?
by angrais 4y ago
>> I've had to write short inductive proofs in several of the systems I've built.
In what context was this necessary?
- recursive 4y agoTo provide evidence that a recursive algorithm actually works maybe?
- eddsh1994 4y agoThis is pretty common in the Blockchain space to verify transactions behave correctly when arriving out of sync with tools like Agda, Coq, etc... I assume it's the same on databases & I heard Leslie Lamport give a talk at work where he mentioned AWS used TLA+ to prove some of its properties.