| ▲ | lallysingh a day ago | |
I'm wondering the inverse, actually. That LLMs can make regular haskell programming (e.g. typing in code, not english that LLMs convert to code) powerful enough to prefer. Can we have LLMs do enough of the grunt work on building type machinery, dealing with compiler errors, looking up exact types and conversion systems, to make the APIs presented to us preferable? So, I could write what I want in haskell, and it's faster for me than to have an LLM do it. The haskell would be high-level enough and precise enough to describe what I want the program to do with less iterations than I'd have with an LLM writing code, finding its own bugs, fixing them, then having me ask it what it did, tell it what to do differently, etc. Direct control is very powerful. LLMs take that away from us, in exchange for a great speedup. But perhaps we can use LLMs to give it back to us by making our actual programming languages more powerful. | ||
| ▲ | calebkaiser a day ago | parent [-] | |
Yeah, I think this is roughly where things are headed. Or at least, it's part of what I'm working on these days, though I'd characterize myself as "generally kind of bad at things," so maybe that's anti-signal. But I think this is actually in the design of many languages already, especially in languages like Lean, where you can prove that the presentable API is correct. Here's one rough example that is related to this direction: A common convention in Lean is to write essentially two versions of a function, with a theorem proving their equality or correspondence. So you can write a more demonstrative version that is more easily understood, which you can treat sort of as a spec that all other implementations must satisfy. And then you can set the agent loose to do whatever nastiness it wants to do to improve performance. Here's a fun write up from someone doing just this with zip file compression: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t... | ||