21–24 of 24 posts
This is cool stuff, but a nitpick: It’s not undefined behavior in the language sense in C to do socket ops on a bad file descriptor. It’s just an error from the kernel’s point of view, and the kernel will throw -errno at you.
Does this work in the face of state changing out from under the socket? I'm not super familiar with low level socket details but I'm thinking something like connect returning EINPROGRESS and you not knowing if the connection has completed. It may complete, it may fail, but during that time this state machine is invalid I think. It seems like strict logical programming like this gets much harder in the face of mutable…
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…