[libre-riscv-dev] formal proof NLnet proposal in

[Luke Kenneth Casson Leighton]

On Monday, September 23, 2019, Hendrik Boom <hendrik at topoi.pooq.com> wrote:

> On Sun, Sep 22, 2019 at 10:12:03PM -0600, Jacob Lifshay wrote:
> > On Sun, Sep 22, 2019, 20:59 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
> > wrote:
> >
> > >
> > > it also ensures that there's no 3rd party that
> > > needs to be approached in an independent audit of the code.
> >
> >
> > not necessarily, we could accidentally test against something that isn't
> > the spec we intended to test against if we misunderstand the spec.
>
> Someone at an IFIP working group once asked us "Would you fly on an
> airplane
> that had been formally proved correct, but never tested?"  No one said
> yes.


:)

That's what riscv-isa-tests are for.
And running linux in an FPGA.
And running the other unit tests.
etc etc.

Strength in depth.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68