ngrislainMar 25

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

https://ngrislain.github.io/blog/2026-3-25-zerocost-posix-compliance-encoding-the-socket-state-machine-in-lean-4s-type-system/

Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean 4's Type System

The best runtime check is the one that never runs.

NGrislain
Show threadkhaledh

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.

[0] https://github.com/khaledh/machina

GitHub - khaledh/machina: An experimental systems programming language

An experimental systems programming language. Contribute to khaledh/machina development by creating an account on GitHub.

GitHub
Mar 25 at 2:40amWeb