[libre-riscv-dev] [Bug 80] Formal Mathematical Proofs needed

bugzilla-daemon at libre-riscv.org bugzilla-daemon at libre-riscv.org
Thu May 2 11:45:04 BST 2019


--- Comment #1 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
cf discussion here:

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.

You are receiving this mail because:
You are on the CC list for the bug.

More information about the libre-riscv-dev mailing list