3 ms·
> where they have formally verified every line of code using the proof assistant Isabelle/HOL. and it's interesting to note that even then, they still had a fe
by jcelerier 8y ago
> where they have formally verified every line of code using the proof assistant Isabelle/HOL.
and it's interesting to note that even then, they still had a few bugs here and there due to incomplete / wrong formalisation
- Koshkin 8y agoAlso, I imagine, automatic theorem provers, too, can have bugs.
- nickpsecurity 8y agoYes. That's the reason the formal methodists started building verified or checkable tools with the checkers being tiny. Doing an solver might involve making it produce a log of each step it made with a simpler system checking them. The checking is also easy to parallelize with linear scaling. My current recommendation is checkable solvers done in a parallel language like Chapel with tiny, verified checkers. Run it logless first to see if it even passes at all. Once passes, run it in logging mode to get evidence to feed to checker. Use multiple, sequential processes to check that as concurrency in checker reduces confidence.