Hacker News new | ask | show | jobs
by pjc50 1018 days ago
You can't really retrofit safety to C. The best that can be achieved is sel4, which while it is written in C has a separate proof of its correctness: https://github.com/seL4/l4v

The proof is much, much more work than the microkernel itself. A proof for something as large as webP might take decades.

1 comments

> A proof for something as large as webP might take decades.

Assuming that it is even provable in the first place.