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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
