Well, yeah, that's not a bad idea. It was kind of Dijkstra's whole thing. The problem is that, at current levels of technology, it's economically better to writ

Well, yeah, that's not a bad idea. It was kind of Dijkstra's whole thing. The problem is that, at current levels of technology, it's economically better to write cheap buggy software than more expensive bug-free software for almost all consumer applications. We are gradually pushing the optimality curve towards the provably bug-free end of the spectrum, but it will take time.