By REALLY careful design, the types are build on a layered
subset of lisp, like Milawa
https://www.cl.cam.ac.uk/~mom22/soundness.pdf
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...)
Cheers,
CY