PS- My default position is that smart contracts are a malware vector.

But if there's some meat on those bones, I wanna know about it. I think of it as a constraints satisfaction problem. If the "vocabulary" can be kept simple enough, where our current theorem provers are sufficient, that could be cool.