> On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly <address@hidden> wrote:
> I previously mentioned the "proof tower" approach to the question
> of proving code at many different layers. Spad code proven in COQ,
> Lisp code in ACL2, and Intel code in CCAs. The missing step in the
> tower was C.
Rather than introduce another complex language and proof problem into the stack, would it be possible to have Lisp implemented directly "on the metal"? If SBCL isn't the preferred approach to such a system, maybe the following project could be used as a starting point to put together a purpose built LISP?
Maybe some of the open source "LISP as OS" projects could offer lower level primitives from which to build the boot strapping code, or a basic set could be defined in x86-64... I suppose it's academic at this point, but I can't help wondering if there would be simplicity gains in the "expressing and defining proof stacks" department that would make it worthwhile in the long run to hold the number of conceptual _expression_ languages down to the minimum necessary.
CY