Well, I think instead of the article's functional utopia, there will be the same pragmatic programming language adoption as in the past. Cutting-edge AI and programming language research is already actively building "auto-formalization" pipelines, which automatically bridge informal requirements and formal proofs; developers provide semi-formal natural language or pseudo-code, and the LLM translates this intent into a hidden formal specification (today like TLA+ or Lean, but likely Event-B or B in the future) to verify the logic; the LLM iterates with the theorem prover in the background and ultimately outputs standard, human-readable code for the developer to review, completely hiding the proof machinery. Expecting the average developer to write or review manual proofs in formal specification languages like Lean or Coq is unrealistic because it demands PhD-level mathematical expertise. Instead of becoming the new standard syntax, formal methods are destined to become an under-the-hood implementation detail.
My prediction is that the "future programming language" won't be a language humans write at all, but rather a dual-layer AI-native Intermediate Representation (IR). Recent experiments have demonstrated that LLMs are already highly proficient at writing and reasoning directly in compiler intermediate languages like LLVM IR. The future compiler stack will likely involve the LLM generating a hyper-minimalist, easily readable syntax for human code review, while silently attaching formal proof annotations directly to the AST for the verifier. The "formal utopia" essentially becomes the new assembly code, entirely invisible to the large majority of engineers.