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.

▲

zozbot234 3 days ago | parent | next [-]

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.

▲

throwawaymaths 2 days ago | parent | prev [-]

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.

▲

gf000 2 days ago | parent [-]

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

	▲	throwawaymaths 2 days ago \| parent [-]
		did i read "above and beyond"