Hi John,
Stephan is traveling and won't be able to respond soon, so I'll try to
answer your question. First of all, you write
How does one say what it means for (certain types of)
numerical programs to be correct?
TLA+ allows you to express mathematics precisely. It doesn't tell you
how to figure out what mathematics you want to express. You write
A simple declarative statement (like Ax = b) at the termination
of an iterative algorithm would be easy to state but impossible
to prove
I presume here A is an array and x and b are vectors, all of reals,
and the problem is that this equality is not going to be ensured by an
algorithm because either (1) it does finite precision arithmetic or
(2) even though it's doing arithmetic with reals, it will not converge
to the correct result in a finite number of iterations. In either
case, you probably want to verify something like |Ax - b| < epsilon
for some suitable epsilon. Numerical analysts have done a lot of work
on this problem--work that I know nothing about. On the other hand,
you spoke about symbolic computation, so maybe you have something else
in mind.
In any case, we'll need to have a better idea of what you want to do
before we can help you. I suggest that we take this off the group
and you reply just to Stephan and/or me.
Leslie