3 ms·

> 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

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

paulddraper 7mo ago
The innovation is making that have zero runtime cost. (Though to be fair, I doubt the runtime cost is really significant...)
- skavi 7mo ago
  Their suggestion is also zero runtime cost.
- jibal 7mo ago
  That's very odd response if you know what a type system is.
hackyhacky 7mo ago
That wouldn't work because there would be nothing stopping you from re-using a value representing an old state.
- ridiculous_fish 7mo ago
  That's exactly what affine / linear types do.