There are basically two ways to make your software amenable to an interactive theorem prover (ITP).
I think you are forgetting to mention the third, and to me “most obvious” way, which is to just write your software in the ITP language in the first place? Lean is actually pretty well suited for this, compared to the other proof assistants. In this case the only place where a “semantic gap” could be introduced is the Lean compiler, which can have bugs, but that doesn’t seem different from the compiler bugs of any other language you would have used.
are you forgetting specification gap between what someone actually wants vs what they say they want vs what someone (else) will actually write in Lean? ..and what they should have wanted if they knew better.. those are still kinds of “semantic gap”, no?
Right, those are all kinds of semantic gaps. Absolutely agreed! Mike Dodds is focused/actively working on these specific kinds of questions, if you’d like to chat about them I recommend emailing him directly :)
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.
I think you are forgetting to mention the third, and to me “most obvious” way, which is to just write your software in the ITP language in the first place? Lean is actually pretty well suited for this, compared to the other proof assistants. In this case the only place where a “semantic gap” could be introduced is the Lean compiler, which can have bugs, but that doesn’t seem different from the compiler bugs of any other language you would have used.
are you forgetting specification gap between what someone actually wants vs what they say they want vs what someone (else) will actually write in Lean? ..and what they should have wanted if they knew better.. those are still kinds of “semantic gap”, no?
Right, those are all kinds of semantic gaps. Absolutely agreed! Mike Dodds is focused/actively working on these specific kinds of questions, if you’d like to chat about them I recommend emailing him directly :)
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.