Re: Catching up on internals

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