Learned helplessness and the languages of DAO
Found on Techcrunch on Sunday, 02 October 2016
Everything is terrible. Most software, even critical system software, is insecure Swiss cheese held together with duct tape, bubble wrap, and bobby pins. See eg this week’s darkly funny post “How to Crash Systemd in One Tweet.” But it’s not just systemd, not just Linux, not just software; the whole industry is at fault.
In principle, code can be proved correct with formal verification. This is a very difficult, time-consuming, and not-always-realistic thing to do; but when you’re talking about critical software, built for the long term, that conducts the operation of many millions of machines, or the investment of many millions of dollars, you should probably at least consider it.
The reason is simple: people don't get paid for writing bug-free code, or have the time. Furthermore, the less common a job is, the higher the chance that someone who wrote software for it does not have a perfect background as a developer.