formal mathematical proofs of all components are needed.
* IEEE754 FPU
* Memory subsystem
* Main processor core
* Boot/IO co-processor
Research to take place in bug #61
cf discussion here:
Hendrik Boom via lists.libre-riscv.org
2:10 AM (9 hours ago)
You not only don't interfere with the device under test, you also don't
let the proof strategy interfere with the statements in the proof.
Which is why the original ML (MetaLanguage) was a type-secure language
with one data type for "theorem" and another for "formula" (i.e.,
something that might or might not ever be proved. It was not originally
intended as a general purpose programming language.
The available operations on 'Theorems" were nothing but the formal rules
for deduction of the logic being used. The rules for "formula" allowed
a lot of tinkering so you could write code to try and figure out a proof
for the thing.
This ancient proof engine was what has later morphed into the ML family
of general-purpose, mostly-functional programming languages, such aas
SML, CAML, OCaml, all of them type-safe by design.