|
|
|
|
|
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. |
|
Assuming that it is even provable in the first place.