Hacker News Reader

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.

View on HN

Windows 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

Also that lines of code is a proxy for rigor, something new I learned today. /s

I think they mean that the code base is small enough to be audited thoroughly. Maybe they should reword it to be clearer.

> 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.

Reply on news.ycombinator.com