If I understood you correctly, I think I'm less extreme than that. Most code written by humans is also not provably correct. But I'm assuming you mean provably correct like Lean: https://lean-lang.org/, and not just "passes tests".
replyIf you mean 'passes tests', that can be tackled by AI. Although AI writing its own tests and then implementing its own code is definitely not a foolproof strategy.
More or less. The tsz solver is pure enough (it doesn't know about the AST) that it might be possible to formally validate it. But in my case I am lucky with tsc baseline. Anything that produces different output than tsc is a bug
reply