Comment by atq2119

I'm always skeptical of claims like these. Ultimately, programming is about writing down instructions for computers to follow. Existing programming languages evolved to be ergonomic for that, proof assistants less so.

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.