
The current state of code generation is making me appreciate theorem provers so much more
watching the industry just blindly accept whatever an autoregressive model spits out is honestly exhausting. we are basically building software on top of glorified autocomplete that just guesses the most likely next token. it feels like mainstream programming is completely forgetting that correctness actually matters
Been messing around with Lean 4 lately just to cleanse my palate. There is something incredibly satisfying about a compiler that just flat out rejects your code if the mathematical proof doesn't close. it forces you to actually design the semantics properly instead of just brute-forcing edge cases with a dozen unit tests
tbh it feels like the only way we survive this flood of probabilistic slop is if we heavily shift our language ecosystems toward strict formal verification as a baseline. was reading earlier about how alternative architectures (like EBMs) are actually starting to max out these theorem proving benchmarks, which is kinda fascinating to see
maybe there's hope that the future of PL design won't just be about generating plausible strings of text, but actually building languages and environments where invalid state transitions are mathematically impossible to express. anyone else diving into proof assistants lately just to escape the madness?