3 ms·
I'm glad to hear that Meta and Google code is "rigorous". I'd prefer INRIA, universities that fund theorem provers, industries where correctness matters like ae
by aksdlf 2y ago
I'm glad to hear that Meta and Google code is "rigorous". I'd prefer INRIA, universities that fund theorem provers, industries where correctness matters like aerospace or semiconductors.
- chc4 2y agoWindows doesn't use the Linux eBPF verifier, they have their own implementation named PREVAIL[0] that is based on an abstract interpretation model that has formal small step semantics. The actual implementation isn't formally proven, however. 0: https://github.com/vbpf/ebpf-verifier https://github.com/vbpf/ebpf-verifier
- auspiv 2y ago[flagged]
- SoftTalker 2y agoAlso that lines of code is a proxy for rigor, something new I learned today. /s
- sunnyps 2y agoI think they mean that the code base is small enough to be audited thoroughly. Maybe they should reword it to be clearer.
- lmm 2y ago> I think they mean that the code base is small enough to be audited thoroughly. They wouldn't say it was "over 20,000 lines" in that case. And 20,000 lines of C is far too big to audit.