| Summary: | Formal Mathematical Proofs needed | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Luke Kenneth Casson Leighton <lkcl> |
| Component: | Hardware Layout | Assignee: | Luke Kenneth Casson Leighton <lkcl> |
| Status: | CONFIRMED --- | ||
| Severity: | enhancement | CC: | libre-soc-bugs |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| 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: | ||
| Bug Depends on: | 61, 158 | ||
| Bug Blocks: | 487 | ||
|
Description
Luke Kenneth Casson Leighton
2019-05-02 00:32:44 BST
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. |