[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Catching up on internals

From: Martin Baker
Subject: Re: [Axiom-developer] Catching up on internals
Date: Sat, 4 Nov 2017 08:38:34 +0000
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.4.0

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


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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]