Hacker News Reader

I think the point is that Fil-C makes programs crash which didn't crash before because use-after-free didn't trigger a segfault. If anything, I'd cite Redis as an example that you can build a safe C program if you go above and beyond in engineering effort... most software doesn't, sadly.

View on HN

Redis uses a whole lot of fiddly data structures that turn out to involve massive amounts of unsafe code even in Rust. You'd need to use something like Frama-C to really prove it safe beyond reasonable doubt. (Or the Rust equivalents that are currently in the works, and being used in an Amazon-funded effort to meticulously prove soundness of the unsafe code in libstd.) Compiling it using Fil-C is a nice academic exercise but not really helpful, since the whole point of those custom data structures is peak performance.

sel4 is the example of building a safe C program if you go above and beyond in effort.

It's provably safer than rust, e.g.

There are obviously multiple levels of correctness. Formal verification is just the very top of that spectrum, but it does comes at extraordinary effort.

did i read "above and beyond"

Reply on news.ycombinator.com