ngrislainZero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types
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.
Interesting take on enforcing state machine rules using a proof system. I'm interested in this space, and have been developing a new programming language to enable typestate / state-machine representation at the type system level[0].
I don't know where it will end up on the spectrum of systems languages; it may end up being too niche or incomplete, but so far I think I'm scratching the right itch, at least for myself.
