[libre-riscv-dev] [Bug 61] Formal Mathematical Proofs needed
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Thu May 2 11:49:07 BST 2019
On Thu, May 2, 2019 at 2:10 AM Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> > you don't "interfere" with the device under test (dut)
>
> 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.
hmmm... intriguing, i can see why it would be done that way.
formal logic was the topic i got a D on at university. i may be
being generous. "For all X there exists nnngh such that..." - i grok
the language... :)
i wonder how far we should go with this.
l
More information about the libre-riscv-dev
mailing list