Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types

Re:Zero-Cost POSIX Compliance: Encoding the Socket State Mac... by wk_end on Tuesday March 24, 2026 @10:32PM (#47512484)

Lean doesn’t have any kind of substructural typing, does it? At a glance it looks like you need to manually (lexically) rebind the socket at each step in the operation, and there’s nothing stopping you from holding onto a socket in a now-invalid state and making mess of things, right?

Also, boo AI slop. If you’re going to use AI to help write your technical blog posts please please please edit out all the “No X. No Y. Just pure Z.” marketing-speak.

[ Parent | on HN ]

Re:Zero-Cost POSIX Compliance: Encoding the Socket State Mac... by tczMUFlmoNk on Tuesday March 24, 2026 @10:59PM (#47512705)

This is what I was thinking, too. Without some kind of linearity, `connect` et al. don't give the claimed guarantees if you can just reuse the old socket handle. Especially if it's aliased in a list or something. I was surprised to see this not mentioned at all in the section specifically dedicated to double-close prevention.

Likewise, with implicit weakening, nothing stops you from dropping the socket without closing it.

[ Parent | on HN ]

Re:Zero-Cost POSIX Compliance: Encoding the Socket State Mac... by ngrislain on Wednesday March 25, 2026 @06:39AM (#47515563)

Yes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.

[ Parent | on HN ]