> Lean 4 offers a fourth option: make the bug unrepresentable at the type level, then erase the proof at compile time so the generated code is identical to raw C.

Couldn't you do that in a more conventional type/class system without using an actual proof system? Instead of there being a Socket type/class, just make a Socket_Fresh, Socket_Bound, Socket_Listening, Socket_Connected, and maybe Socket_Closed (not 100% sure, would have to think about whether that's a thing or not), each of which takes the previous in its constructor. Or does that make it too hard to use?

That wouldn't work because there would be nothing stopping you from re-using a value representing an old state.

The innovation is making that have zero runtime cost. (Though to be fair, I doubt the runtime cost is really significant...)