One of the things I’ve noticed moving from C (and Objective-C) to languages like C++ and Rust, with richer static type systems is that it changes what most of the code is for.
When I write C code, almost all of my code is to do the thing. When I write the same in C++, I can usually do the thing in about half as much code. But I don’t write half as much code. The other half of the code is making sure that’s if the code doesn’t do the thing, it probably won’t compile. If I have a field that needs accessing with a lock held, I’ll write an accessor that takes a lock guard to prove lock ownership, and a wrapper that acquires the lock and returns the lock guard and a reference to the field. This compiles down to the same code as the C version (except maybe in debug builds, where I’d assert that the lock guard is really for the right lock), but now it’s harder to get wrong. Especially when I come back to the code in two years and don’t remember to read the comment telling me the locks I need to hold to access the code.
This is why I’m excited by Verus for Rust: it gives me a very rich set of tools for ensuring that my code is going to do the right thing. But it’s a big mindset shift from ‘code exists to do the thing’ to ‘doing the thing is the easy part, most of the code exists to make sure you’re not doing the wrong thing’. And I suspect that’s both why it’s hard for people to switch from C and why few people who do ever want to go back.
When I write C code, almost all of my code is to do the thing. When I write the same in C++, I can usually do the thing in about half as much code. But I don’t write half as much code. The other half of the code is making sure that’s if the code doesn’t do the thing, it probably won’t compile. If I have a field that needs accessing with a lock held, I’ll write an accessor that takes a lock guard to prove lock ownership, and a wrapper that acquires the lock and returns the lock guard and a reference to the field. This compiles down to the same code as the C version (except maybe in debug builds, where I’d assert that the lock guard is really for the right lock), but now it’s harder to get wrong. Especially when I come back to the code in two years and don’t remember to read the comment telling me the locks I need to hold to access the code.
This is why I’m excited by Verus for Rust: it gives me a very rich set of tools for ensuring that my code is going to do the right thing. But it’s a big mindset shift from ‘code exists to do the thing’ to ‘doing the thing is the easy part, most of the code exists to make sure you’re not doing the wrong thing’. And I suspect that’s both why it’s hard for people to switch from C and why few people who do ever want to go back.
3