[libre-riscv-dev] Freedom Critical [was: Long, probably pointless]

[Scheming Pony]

>> regarding "getting back to instant on", this is what bare metal testing does.
> I believe the Gambit implementors have set up a PC that boots directly into the Gambit repl instead of using an intermediating operating system

Mezzano OS (Common Lisp) boots to a raw VM, (there have been other efforts including a CL Linux kernel module):
https://github.com/froggey/Mezzano

Scheme48 has an interesting systems language called Pre-Scheme, which supposedly has been mathematically verified.  There are also other efforts using Scheme like C.
https://en.wikipedia.org/wiki/Scheme_48#Implementation

Vis-a-vis bare metal testing, at Boeing I worked on the development of an airborne, safety critical Ada compiler / VM for navigation which was run on a bare metal dev board.  I was involved in formal VM development, formal testing, documentation, and bootstrapping the VM to a microprocessor, and got a debug monitor working through JTAG.  I learned a lot about safety critical testing and development.  Part of the FAA DO-178 software certification requires source/object code traced to requirements, and testing using techniques like MCDC path coverage.

https://upload.wikimedia.org/wikipedia/commons/4/4f/DO-178B_Process_Visual_Summary_Rev_A.pdf

Since the project we are working on here is "freedom critical", perhaps some of the ideas would carry over.

I read through a lot of the source for MIT/Scheme to get page up/page down working in Edwin (creating the world's loneliest patch), and saw stuff like a "microcode" subdirectory--makes you wonder...  There is also the famous MIT AI Memo 514 by Steele/Sussman and the Scheme-81 chip.

sjm