"Provable" essentially means, you have explicit operators acting on explicit states in an exhaustively defined way that preserves "truth", explicitly defined invariants.
A finite thing you can argue over deterministically.
Obviously, "you" there is an LLM, the machine your code is run on has to be defined in that very same exacting manner and so on.
That still isn't enough, you need abstraction, a hierarchy of categories that preserve your intent and accurately describe the problem space.
"Programming" then is solving an inverse problem over that hierarchy, filling in the blanks sensibly on your way down through the model hierarchy, all the way to atomic instructions your (proven) hardware understands.
Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.
All of which is to say: yes, the current state is a mess. Resolving that is far from easy.
But you really have no choice, that mess is transparent to large-enough LLMs. Security by obscurity only goes so far.