[libre-riscv-dev] Freedom Critical [was: Long, probably pointless]
scheming-pony at protonmail.com
Tue Feb 18 10:25:20 GMT 2020
>> 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):
Scheme48 has an interesting systems language called Pre-Scheme, which supposedly has been mathematically verified. There are also other efforts using Scheme like C.
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.
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.
More information about the libre-riscv-dev