[yjftsjthsd-h]

> 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?

[hackyhacky]

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

[ridiculous_fish]

That's exactly what affine / linear types do.

[paulddraper]

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

[skavi]

Their suggestion is also zero runtime cost.

[jibal]

That's very odd response if you know what a type system is.