2022: We need end-to-end certified compilation!
2024: Nah, just stuff your "proofs" into an LLM to get "executables".

x.com/VictorTaelin/status/1837

> 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.

@dpwiz That's interesting, do we know why are they migrating from Agda to JavaScript?

For reference, here is the compiler prompt: github.com/VictorTaelin/AI-scr

Follow

@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.

Sign in to participate in the conversation
Qoto Mastodon

QOTO: Question Others to Teach Ourselves
An inclusive, Academic Freedom, instance
All cultures welcome.
Hate speech and harassment strictly forbidden.