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

[Luke Kenneth Casson Leighton]

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