Mastodawn

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 thread

wk_end

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.