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

[Hendrik Boom]

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.

-- hendrik

> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev