Comment by auggierose
5 days ago
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
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.
Back when I first studied this 20 years ago the progenitors predicted it would get very popular one day.
What actually happened was that some programming languages borrowed a few concepts and life carried on as before.
I started with this 30 years ago, so yeah, I know the history :-) This time is different.