On 04/11/17 00:42, Tim Daly wrote:
On the other hand, my current effort involves proving Axiom correct. That
should (in theory) eliminate whole classes of errors. This is at the expense
of proving new code correct which tends to get a negative reaction from
developers.
Tim,
I know little about proving code correct (though it looks like an
interesting topic) so I'm certainly not doubting anything you say. Its
just that (in my ignorance) I would have thought it would have been
easier to prove high level code correct than low level code and
therefore, for this reason, better to move boot code to SPAD than Lisp?
By 'high level code' I mean code with meaningful static types and
semantics closer to mathematical structures.
Martin B
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
