[angrais]

>> I've had to write short inductive proofs in several of the systems I've built.

In what context was this necessary?

[eddsh1994]

This 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.

[recursive]

To provide evidence that a recursive algorithm actually works maybe?