That’s a good point. Maybe I’m naive, but I think my (very strong) prior is that we are basically locked in to Python and Typescript as the de norm programming languages for normie vibe-coders for the foreseeable future, for a number of reasons including ease of novice human code review, model expertise in these languages, and rapidly proliferating infrastructure and libraries to support vibing in these languages, and thus the challenge is to take such pre-existing code and somehow “bring it in” to the ITP. But you are of course correct that someone could find a way to make it easy and fun for non-FM-pilled engineers to vibe traditional software directly in Lean, and this would simplify things greatly.
This might be not too crazy, but I am not too familiar with Lean.
How different is Lean from other well established strongly typed languages, like e.g. Rust? If you can set up an “ecosystem mover” LLM, where you port the whole libraries to Lean, that would be a good starting point.
That’s a good point. Maybe I’m naive, but I think my (very strong) prior is that we are basically locked in to Python and Typescript as the de norm programming languages for normie vibe-coders for the foreseeable future, for a number of reasons including ease of novice human code review, model expertise in these languages, and rapidly proliferating infrastructure and libraries to support vibing in these languages, and thus the challenge is to take such pre-existing code and somehow “bring it in” to the ITP. But you are of course correct that someone could find a way to make it easy and fun for non-FM-pilled engineers to vibe traditional software directly in Lean, and this would simplify things greatly.
This might be not too crazy, but I am not too familiar with Lean.
How different is Lean from other well established strongly typed languages, like e.g. Rust?
If you can set up an “ecosystem mover” LLM, where you port the whole libraries to Lean, that would be a good starting point.