4 ms·

I'm not recommending frama-C, I'm opining on what's necessary to write reliable C code. Much of Rust's complexity is not directly addressing memory safety, it'

• 0815test 7y ago
  "A C-with-borrow-checker" is a good-enough description of Cyclone, which is not that different from Rust and which was basically abandoned for Rust. Sure, Rust itself has a number of higher-level features, some of which are a bit problematic by comparison with C (e.g. monomorphizing generics lead to intermediate-code bloat, which causes long compile times) but it turns out that these features are practically needed, either to make programming-in-the-large more feasible or to abstract some underlying details from user-level Rust code so it can keep working even as the compiler and standard library evolve underneath it. C doesn't have these problems being a mature platform, but Rust still does.