Well, then the solution there is to only write trivial programs. Haha. Though, with enough resources, time, and effort, I think almost any program one would wa

Well, then the solution there is to only write trivial programs. Haha. Though, with enough resources, time, and effort, I think almost any program one would want in practice could be written with a formal proof of correctness. (I won't say every, because that runs up against halting problem / incompleteness things, but I think for almost all that you would actually want) It's just that there isn't enough demand, and time, for the programs to be proven correct. If there was a program that we could all stand to wait for a very long time for (maybe even a few generations?), and it was important enough that it be completely free of bugs, that could be done, I think. I'm not sure what it would be that important though. Starship stuff?