News for hackers. Stuff that matters.

A comment on Lean proved this program correct; then I found a bug. Parent comment

Re:Lean proved this program correct; then I found a bug by monocasa on Monday April 13, 2026 @11:46PM (#47761013)
Totally agreed. For instance that's why sel4 just throws the whole binary at the proof engine. That takes any runtime (minimal in sel4's case) and compiler (not nearly as minimal) out of the TCB.
[ Parent | on HN ]

There are no comments on this comment yet.