For example, Ron Pressler seems to think that writing software
is beyond the difficulty of anything we've previously tried to do
and that math (alone) won't help us.
https://pron.github.io/posts/correctness-and-complexity
Using fundamental results from Godel and Turing, Ron seems
to show that software verification can't succeed. He may be
right in the general case.
Thanks for that link - I had seen that video, but didn't know (or had forgotten about) the write up. I found that talk extremely interesting. What it seems to make an excellent case for is that we're never going to get to a point where we are bereft of practical challenges getting computers to do what we want them to - the limitations of mathematics and computers fundamentally preclude it when we tackle complex problems. (Fortunately that doesn't mean it isn't worth attempting to get things right anyway - it just lets us manage expectations both of people and outcomes when we try.)
Axiom isn't the general case. At least some of the algorithms
encode mathematics, a small subset of the universe of Ron's
argument and one where verification seems possible.
That makes sense to me. One of the takeaways for me from that talk was *not* that all formal efforts are ultimately futile - only the attempts to completely eliminate all errors of any type. Instead, the useful activity is to focus on applying such techniques to progressively eliminate the more probable failure modes (what he terms "common and costly bugs") observed in real world systems to improve the chances of successful user outcomes.
Axiom is by design and intent focused on mathematics - i.e. that portion of the Venn diagram which is provable. Because it must be a computer program running on a computer system there will always be some uncertainties (if nothing else we are dependent on correct behavior of the hardware, which is subject to entropy over time) but the *exact* same thing is true of humans. What a Computer Algebra System can ultimately provide (in theory) is to exploit a computer's deterministic, reproducible information manipulation to be more accurate than anything a human brain could achieve on its own, and that is of immense practical value. The running (indeed infinite) challenge is to see how low failure rates can be pushed practically, and formal systems provide a framework within which to do that pushing.
CY