2022: We need end-to-end certified compilation!
2024: Nah, just stuff your "proofs" into an LLM to get "executables".
https://x.com/VictorTaelin/status/1837925011187027994
> Since the AgdaJS compiler isn't maintained, and since creating one would be a $1m-budget project, we're now compiling 590 Agda files to TypeScript using Sonnet-3.5, to let us run our apps on the browser.
> The results are excellent. Almost all files work with no intervention. Error rate is lower than the current AgdaJS compiler, on which we found bugs. Performance is 20x higher. We're now automating this in a loop.
@tristanC They aren't migrating if I understood correctly. Just need a way to produce TS apps from Agda sources and LLM translation happens to do a better job at it than a "real" compiler.
@dpwiz That's interesting, do we know why are they migrating from Agda to JavaScript?
For reference, here is the compiler prompt: https://github.com/VictorTaelin/AI-scripts/blob/main/agda2ts.mjs