I think we’re coming at correctness from two different perspectives.
You’re treating it as an engineering concern - whether we can statically prove properties of the code itself. And you’re right that outside the Idris/Lean/Agda circle, formal program correctness is largely out of reach.
I’m treating it as an operational concern - does the application do what it was designed to do? Not what it does mechanically, but whether it actually does the thing the user asked for. That’s a different question. I wouldn’t try to answer it with static analysis. I’d answer it with executable acceptance criteria that get re-verified on every commit.
So when I say “correctness first,” I’m not asking for a tool that proves all code in some general sense. I’m asking for a way to keep the application bound to the intent it was built to satisfy. The downstream concerns (architecture, security, code quality) get much easier to address once you can verify intent on an ongoing basis - because they’re no longer load-bearing for whether the thing works.
