I haven'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'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.

It would be fantastic if I could casually throw in a proof while debugging a hard problem.