Earlier quoted context omitted.
Same is true for blockchain smartcontracts, which have similar catastrophic consequences.
That truly is scary to me. I can easily* write advanced Solidity and could try to make something big. But I won't, because I know I would not be able to handle the stress and responsibility. One tiny logic error and millions lost. Thanks but no thanks. *The fact I believe I could easily do it is probably exactly why I'd end up making some huge mistake. ;)
Maybe if you could translate from Coq.