[Axiom-developer] PVS

[daly]

Thanks. I had not heard of PVS but I will look into it.

I have used ACL2 in the distant past and will have to get up
to speed on it again. I've downloaded and built the latest version.

I know that ACL2 is not capable of handling a Spad compiler but one
has to start somewhere. The important point, in my mind, is the focus
on some sort of proof in the long term.  We really need to have a
higher standard for computational mathematics, and, as they say,
"If not us, who? If not now, when?".

Matt Kaufmann and J Moore have always been quite helpful in the
past. I suspect they would be interested in any work we do in
this area.

Tim Daly