What I do not understand with the "languages do not matter"/"frameworks do not matter" is ultimately the following:

What a good language or a good library (and to a lesser degree also a good framework) does is to pre-compress ideas into well understandable and composable chunks.

Examples:

`printf("foo %d, %3.2f %s", ...)` abstracts/compresses a general strategy of shuffling bytes into the correct ascii/utf-8... format. An LLM could also write the raw assembly or bytecode for doing the same thing, but for one it would take much more tokens and to apply this pre-invented concept, and second without the concept already invented there would be no "information pattern" in existence that the LLM could have learned or refer to.

`list.map(...).filter(...)...` are patterns that (when applied strictly in a functional sense) go hand in hand with laws like `map` not affecting the number of elements, and filter producing no new elements etc... These are also patterns that are already invented and depending on the language these restrictions are checked. Just reading `map` somewhere can tell you (and the LLM) a lot, and writing `map` instead of while, for or jmp will capture and express much more information. LLMs would not have been able to learn these concepts if they did not already exist. And even if such a general pattern would be discovered by an LLM somewhere inside its learnt parameters, it would not haven given this pattern a name that it could/would tell you. And if you do not know the name for such a concept how have a much harder time prompting the LLM.

Expressing computations in a well understood algebra allows for symbolic manipulation and simplification. like `5 + 3 == 3 * 5 == (1+1+1) * 5 == (5+5+5)...`. But algebraic manipulation requires a symbolic language with precise rules to describe what manipulation is allowed. In AI-speak you could say the language itself is a harness or a sandbox to guide and restrict whats possible. Doing advanced math proofs is only possible for LLMs because languages like LEAN provide a strict guideline to build upon.

In short, two extremes: If LEAN is so great at proofing correctness and LLMs are so good at LEAN, why is not from today on everything (windows, linux, basecamp, hey, gcc, rustc, blender...) translated into LEAN? Why bother with rust at all? On the other hand if languages do not matter anyway and LLMs are able to recognize all the pattern on their own, why not let the LLM output and iterate on the binary bytecode to generate a self contained binary directly?