Of particular interest is clarity.
I've been working with LEAN. The code is in C++ and is very
clever. For instance, there is a beautiful macro embedded in
data structures to perform reference counting.
Unfortunately, I can't reverse-engineer the logic rules that are
embedded in the C++ code.
Tim,
I can see how you can prove individual algorithms correct and I can see
how you can use a proven Lisp but, if you want to prove "down to the
metal", it looks to me like there is an enormous gap in-between which is
SPAD.
Can you really prove SPAD correct?
You mention a specification
