Comment by acobster

> In theory we could build a framework that makes it easy to write loophole-free contracts

You mean similar to how, in theory, we could build a framework that makes it easy for us all to write readable, bug-free code?

Edit: I was mostly being tongue in cheek, but I also recognize that this is about provably correct code à la Coq, etc. That'd be cool for sure. :)