Given there is before and after code, perhaps the translation can be automated. If the whole code base were auto-translated, what bugs could be detected and fed back to the C implementation? I'm assuming there is going to be hesitance from the FreeBSD community from migrating their codebase from C to Checked C, but that doesn't mean this work needs to come to nought. On top of bounded memory accesses, it'd be interesting to see better thread, signal, interrupt, etc. safety support. I guess at some point this just looks like Rust.