I predict in 10 years „code“ that is not actually in the language of a proof assistant will be the exception, not the norm. This will happen by proof assistant languages becoming easier to the point that normal code will look cumbersome
And having meta language that is significantly different from the core language really sucks for ergonomics. I never understood why, for example, a lot of dependent types literature invents a meta language for expressing constraints rather than using the core language for it. Syntactic familiarity matters.
Also consider C++ templates vs Zig comptime, and how C++ is evolving to bring its meta language closer to the core language via constexpr and consteval.
So the more viable path is to judiciously integrate formal concepts into "normal" programming languages and have LLMs generate proof artefacts in a search process that is guided by proof systems.
What actually happened was that some programming languages borrowed a few concepts and life carried on as before.