Bug 80 - Formal Mathematical Proofs needed
Summary: Formal Mathematical Proofs needed
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Hardware Layout (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
Depends on: 61 158
Blocks: 487
  Show dependency treegraph
Reported: 2019-05-02 00:32 BST by Luke Kenneth Casson Leighton
Modified: 2020-09-10 01:23 BST (History)
1 user (show)

See Also:
NLnet milestone: Future
total budget (EUR) for completion of task and all subtasks: 24000
budget (EUR) for this task, excluding subtasks' budget: 24000
parent task for budget allocation: 487
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2019-05-02 00:32:44 BST
formal mathematical proofs of all components are needed.

* libraries
* Memory subsystem
* Main processor core
* Boot/IO co-processor

Research to take place in bug #61
Comment 1 Luke Kenneth Casson Leighton 2019-05-02 11:45:04 BST
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.