[Top][All Lists]

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

Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings

From: Clifford Yapp
Subject: Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings
Date: Sun, 30 Jun 2019 15:18:29 -0400

On Sun, Jun 30, 2019 at 11:40 AM Tim Daly <address@hidden> wrote:

By REALLY careful design, the types are build on a layered
subset of lisp, like Milawa
which is sound all the way down to the metal.
Milawa and Jitawa... Wow.  That is a really interesting development.

Tim, I'm nowhere near current on recent developments so apologies if I'm not interpreting this correctly, but will the Sane core be able to identify any existing bugs in the Spad code?  I.e., will any successful compilation of existing Spad code on the Sane stack indicate verified correctness of the Spad algorithm?  Or (almost as useful for applied problems) will it instead mean that for any particular application of a Sane-compiled Spad algorithm to a specific numerical problem, the system will be able to generate a specific proof for the correctness of that answer that is in turn tractably verifiable by simple proof checkers?

(Either way, what I'm hoping is that whether or not proof techniques are powerful enough to verify general properties of symbolic expressions, this approach will allow an applied user (say a physicist) to at the end of the day be very confident that the computer-algebra-system-supplied answer for any specific problem is correct...)


reply via email to

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