alt Hacker Newsnot of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.
Replies
streetfighter64 • today at 1:09 PM
It holds that ¬(∀subsets: isverified(subset)) but it's not true that ∀subsets: ¬isverified(subset), which it think most people would interpret "the whole system is unverified" as
➕ show 1 reply
The eventual goal is verification of the full system. Not the implementation, yes, that's infeasible. But this will mean all soundness bugs will be either found and fixed or we'll know how to fix them once they're found. In any way they won't be fundamental (which is believed to be the case today, but not proven).