Comment by Groxx
20 hours ago
I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems.
I don't really think that works either, because there's endless ways to add complication even if you can't worsen behavior (assuming that's even possible). At best they might be caught eventually... but anyone who has worked in a large tech company knows at least a few people who are somehow still employed years later, despite constant ineptitude. Play The Game well enough and it's probably always possible.
It's even conceivable that 2 gets worse with AI: The AI does the proof for them, very convolutedly so, and as long as the proof checker eats it, it goes through. Comes the day when the complexity goes beyond what the AI assistant can handle and it gives up. At that point, the proof codes complexity will for a long time have passed the threshold of being comprehensible for any human and there is no progress possible. Hard stop.
Using a proof language with an SMT solver is basically that: an inexplicable tick that it’s fine, until a small change is needed, the tick is gone, and nothing can say why.
That's basically what sledgehammer (mentioned in the article) boils down to. The Lean folks use some safeguards to avoid issues with that, such as only using their "grind" at the end of a proof, where all the "building blocks" have been added to context.