It is definitely possible, to what practical scale is the question.<p>And you need to define what failure actually means.<p>eg while the software might not fail, the specification very well might, meaning the software does exactly as asked, but asked to do something that creates an overall failure.<p>Many failures relate to specification, not execution. Failure in specification is the very difficult problem to solve.<p>But even just looking at the software component, it would involve coding everything from the ground up, generating code from specifications proven by formal methods and so on. Likely meaning no third party libraries.<p>The code generation tools themselves would require specification and validation by formal methods.<p>You could rapidly end up at a place where easily your greatest risks were hardware failure or hacking.<p>As someone who designs safety critical systems for a living, most code created these days is on a "near enough" basis and the benefits are so immense that occasional downsides are tolerable.<p>So we have evolved to a quagmire for consumer grade software that will never get any better without a total restart or rethink, but that is probably ok, because the benefits far outweigh the risks, in general.<p>Think about something slightly similar. The risk of dying in a car or bike incident is very real, but if you asked anyone would they rather take that risk or walk everywhere, they would happily take the risk.<p>Same as people doing their banking on PC.
Plus, in the PC banking context, other systems have evolved outside to ameliate that risk. (eg ability of the banks to roll back transactions).
So the cost of seeking ultimate infallibility just isn't worth the results.<p>Ultimately, everything is a trade-off.
When I read this, I was like... I'm pretty sure DJB has done this a few different times.<p>Damn do I miss the days of qmail.<p><a href="https://cr.yp.to/qmail/guarantee.html" rel="nofollow">https://cr.yp.to/qmail/guarantee.html</a>
Long-long time ago, at a Munich University, I remember Prof Schwichtenberg, who worked on software extraction from from mathematical proofs (in Scheme).<p>The idea is to prove that the software works.
yes, it's possible. I think it's called formal verification.<p><a href="https://en.wikipedia.org/wiki/Formal_verification" rel="nofollow">https://en.wikipedia.org/wiki/Formal_verification</a><p>I can't even begin to understand how it's done. I suspect we need a new programming language that forces you to do it before it compiles to machine code. or an AI that's setup to prove what you code.
it is impossible. You can put really hign testing standards and principles to make the software really safe but you can never prove a complex system never fails or can't be hacked. The tradeoff is that changes will be very very slow and expensive. This is needed for mission critical systems but an overkill for most consumer softwares as you won't survive the market with this approach.