Comment by hrmtst93837
7 hours ago
People treating this as a scaling problem are skipping the part where verification runs into undecidability fast.
Proving a small pure function is one thing, but once the code touches syscalls, a stateful network protocol, time, randomness, or messy I/O semantics, the work shifts from 'verify the program' to 'model the world well enough that the proof means anything,' and that is where the wheels come off.
Or anything where the interaction of small pure functions matters. NAND is a simple pure function. 6 NANDs connected correctly gets you a D flip flop, and suddenly you've got state. Bugs can hide in the combinatorics of all the possible states of your system, and you'll never test them all in polynomial time.