cf discussion here:
http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2019-May/001369.html

Hendrik Boom via lists.libre-riscv.org 
2:10 AM (9 hours ago)

to libre-riscv-dev


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.