I haven&#x27;t used Idris, but it sounds like someone I might want. I really want a tool that lets me mix and match operational code with proofs. It&#x27;s common now to write a unit test while debugging something, less common to write a randomized property tester, and rare to see a theorem prover being used.<p>It would be fantastic if I could casually throw in a proof while debugging a hard problem.