Leslie Lamport has a model-checking language TLA+ which looks like it might be useful for proving the interpreter correct. A free online book is available at: http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
Tim "If it's free, it's for me" _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer