Speaking of formal verification of software, I note that in the blockchain community, “smart contract” enthusiasts are now discovering that they might need some serious rigor in their executable contracts. A few slight problems, such as the complete collapse of The DAO, due to, well, logical bugs in the “smart” contracts.
The goal of “smart” contracts seems to be to eliminate those faulty and dishonest carbon based units, in favor of the cold, clean, logic of machine code. In their naïve enthusiasm, many people seemed to think that a Turing complete language is a good thing for these contracts, apparently knowing little about formal logic or languages.
Anyway, most people now realize that writing executable contracts is difficult, and, no matter how smart you think you are, you probably can’t write perfect code, at least not without assistance. So, let’s use formal verification to, as Pete Rizzo puts it seek “smart contract certainty”.
Rizzo is reporting on the Ethereum developers summit , which was said to be a lot more sober this year, after their catastrophic spring. Rizzo indicates that multiple speakers discussed formal verification, “as a way to inspire confidence” in the software and protocols.
They are certainly correct that formal logic must play an important role in this technology, and I suppose that it might be a valuable sandbox for formal tools. (Of course, this is hardly news to Wall Street. Financial wizards already employ clever logicians, who don’t really talk about what they do to earn their millions.)
My own view is that formal logic may help reduce stupid bugs, though it will generally make the systems opaque beyond human comprehension. This is a really bad thing for the overall goal of assuring that the contracts do what the people want them to, and any confidence in such systems may well be misplaced. If you can’t understand it, how can you trust it?
As the joke goes, “Let me make you an offer you can’t understand”.
In any case, these contracts must exist in the real world, which is neither on-line nor formally verified. I think that the big problem with many financial systems isn’t that the contracts aren’t executed accurately, but that the contracts are rigged by the rich to rob the poor. Automating the process is scarcely a solution to that problem, at least not for us poor people.
It will be interesting to see what can be done in this area. Can you actually create “provably correct” executable contracts that (a) are believable and (b) do something nontrivial.