On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <axiomcas@gmail.com> wrote:

For example, Ron Pressler seems to thi= nk 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 t=
hat link - I had seen that video, but didn't know (or had forgotten abo=
ut) the write up.=C2=A0 I found that talk extremely interesting.=C2=A0 What=
it seems to make an excellent case for is that we're never going to ge=
t 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 f=
undamentally preclude it when we tackle complex problems.=C2=A0 (Fortunatel=
y that doesn't mean it isn't worth attempting to get things right a=
nyway - it just lets us manage expectations both of people and outcomes whe=
n we try.)

=C2=A0

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.=C2=A0 One of the takeaways for me from=
that talk was *not* that all formal efforts are ultimately futile - only t=
he attempts to completely eliminate all errors of any type.=C2=A0 Instead, =
the useful activity is to focus on applying such techniques to progressivel=
y eliminate the more probable failure modes (what he terms "common and=
costly bugs") observed in real world systems to improve the chances o=
f successful user outcomes.

Axiom is by design and=
intent focused on mathematics - i.e. that portion of the Venn diagram whic=
h is provable.=C2=A0 Because it must be a computer program running on a com=
puter system there will always be some uncertainties (if nothing else we ar=
e dependent on correct behavior of the hardware, which is subject to entrop=
y over time) but the *exact* same thing is true of humans.=C2=A0 What a Com=
puter Algebra System can ultimately provide (in theory) is to exploit a com=
puter'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.=C2=A0 The running (indeed infinite) challenge =
is to see how low failure rates can be pushed practically, and formal syste=
ms provide a framework within which to do that pushing.

=C2=
=A0

CY