[Axiom-developer] Computational Mathematics, proofs, and correctness

[daly]

Waldek,

>The real question is how to do this.  Several years ago
>my student did "by hand" a proof in Hoare logic of a simple 20
>line long program.  The proof is 20 pages long.  The proof
>is rather detailed, but he consided some facts as known
>and some readers probably would ask questions demanding
>more details.

Was this proof published anywhere? Do you have a URL?

Tim