3 ms·
We might see wider adoption of dependently typed languages like Agda. But limited corpus might become the limiting factor, I’m not sure how knowledge transfers
by seanmcdirmid 1y ago
We might see wider adoption of dependently typed languages like Agda. But limited corpus might become the limiting factor, I’m not sure how knowledge transfers as the languages get more different.
- ipnon 1y agoIt's getting cheaper and cheaper to generate corpora by the day, and Agda has the advantage of being verifiable like Lean. So you can simulate large amounts of programs and feed these back into the model. I think this is a major reason why we're seeing remarkable improvements in formal sciences like the recent IMO golds, and yet LLMs are still struggling to generate aesthetically pleasing and consistent CSS. Imagine a high schooler who can win an IMO gold medal but can't center a div!
- andrewflnr 1y agoIt seems like "generating" a corpus in that situation is more like a search process guided by prompts and more critically the type checker, rather than a straight generation process right? You need some base reality or you'll still just have garbage in, garbage out.