Quoting Dijkstra (1988, EWD1036):
... a program is no more than half a conjecture. The other
half of a conjecture is the functional specification the
program is supposed to satisfy. The programmer's task
is to present such complete conjectures as proven theorems.
Axiom's SANE research project
I occasionally get grief because Axiom is implemented
in Common Lisp. People don't seem to like that for some
odd reason. Lisp, one of the easiest languages to learn,
seems to be difficult to accept.
I'm working with John Harrison's book "Practical Logic
and Automated Reasoning" from 2009. It
