[Libre-soc-dev] maybe get ryzen 7950x for faster compilation and avx512

[Jacob Lifshay]

On Tue, Sep 27, 2022 at 6:18 PM Jacob Bachmeyer <jcb62281 at gmail.com> wrote:
>
> Jacob Lifshay wrote:
> > OpenSSL is not a good example because there were no tests for
> > Heartbleed, whereas we do have formal proofs (they automatically cover
> > all corner cases if written correctly; OpenSSL did not have formal
> > proofs that could have caught Heartbleed) and unit tests that can be
> > relatively easily run by others.
>
> None of that matters if no one who can understand the issue actually
> looks at it.

true, but formal proofs don't require reading the code they're proving
(not the proof itself) in order for them to detect anything that
doesn't satisfy the proof. this means others can just run the formal
proofs themselves -- this is pretty easy with gitlab ci -- just upload
to any gitlab instance with a runner that has sufficient ram and a
long enough timeout. My point is merely that OpenSSL isn't a good
example, not that your point is invalid.

Jacob