I've discovered something pleasant about CLOS development.
Normal compiler development is top=down, from the syntax to
the intermediate representation to the target machine. By its
nature the intermediate representation is usually a hairy data
structure.
However, CLOS is both a surface syntax and
When injured, I often use the phrase "Well, learning occurred".
I just spent the last day chasing a circular reference problem
in the meta-object protocol (MOP) which is the basis of the
Common Lisp Object System (CLOS). It turns out that the
"circular reference" is a REALLY bad error message. It
Martin,
> Are there some fundamental compromises that have to be made when combining
> computer > algebra and proof technology?
> For instance in proof assistants, like Coq, equations are types for instance:
> x = x + 0
> is a proposition which, by Curry-Howard, can be represented as a type. T
On 19/06/2019 12:18, Tim Daly wrote:
The effort to
Prove Axiom Sane involves merging computer algebra and proof
technology so Axiom's algorithms have associated proofs.
Tim,
Are there some fundamental compromises that have to be made when
combining computer algebra and proof technology?
For
Sane: "rational, coherent, judicious, sound"
Axiom is computational mathematics, of course. The effort to
Prove Axiom Sane involves merging computer algebra and proof
technology so Axiom's algorithms have associated proofs.
The union of these two fields has made it obvious how far behind
Axiom ha
