Okay,
I looked at intel.pdf and brought to mind a crosscompiler I wrote way
back when. Convincing a PDP-8 compiler to generate object code for
something like a 6809. It's vague but I am convinced I was looking at
object code and outputting differrent object code. Or some such but
neverthel
>You will have to excuse me if I dozed off in the back seat during the
>trip. Is this where we are?
We're still lost but things have changed a bit since the 80s.
>We have a programming language (say SPAD or lisp) and a program in
>that language represented by a series of statements.
>The intent
You will have to excuse me if I dozed off in the back seat during the trip.
Is this where we are?
We have a programming language (say SPAD or lisp) and a program in that
language represented by a series of statements.
The intent is to construct, in a literate manner, a series of statements
in MP
Axiom has moved into a new phase. The goal is to prove Axiom correct.
There are several tools and several levels of proof. I've added
the machinery to run proofs in COQ (for algebra) and ACL2 (for
the interpreter and compiler).
One of the first steps for the algebra proofs involves decorating
the
