On Sun, Jun 30, 2019 at 11:40 AM Tim Daly wrote:
>
> 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
There are thousands of hours of expertise and thousands of
functions embedded in Spad code. An important design goal
is to ensure that code continues to function. The Sane compiler
will output code that runs in the interpreter. It is important that
"nothing breaks".
That said, the Sane compiler is
Tim,
This all seems to be about the lisp layer, obviously thats what
interests you.
It seems to me that if SPAD code is complicated and not aligned to type
theory then, when SPAD is complied to Lisp, the List code will be
complicated and hard to work with. Your previous remarks, about not
s
