Earlier quoted context omitted.
um... use dependent types? sorry but I'm from different language background :(
Provable code would solve the root cause, yes. :) However, even with provable code, the proof actually has to be both correct and performed. There are too many competing factors that won't allow idris, for example, to actually work. The result is that, as an industry, the Internet and the world's business are held together by twine, twist ties, and spaghetti code. Even this very webpage is just enough to work for mos…
(but... I'd be jobless if that were to happen :(