Transpiling code

Stream: Machine Learning for Theorem Proving

[Jason Rute]

This is Agda and not Lean, but this tweet is really interesting. He massively transpiles code from Agda to TypeScript using a LLM (Sonnet 3.5). I wonder how much it works in practice and scales. https://x.com/victortaelin/status/1837925011187027994?s=12

[Jason Rute]

I think this is @Victor Maia of KindLang (mentioned elsewhere here).

[Xiyu Zhai]

With these as test cases, how hard will it be to let Sonnet maintain an actual transpilot

[Bas Spitters]

Is there any feedback from the type checker to the AI?

[Jason Rute]

@Bas Spitters I don’t think so, but possibly there is some filtering to check if it actually compiles to TypeScript and maybe even some iteration to fix errors. Here is the prompt and code: https://github.com/VictorTaelin/AI-scripts/blob/main/agda2ts.mjs Also, he wasn’t clear how much manual fixing he had to do.