Re:A technical vision for the Haskell ecosystem
by calebkaiser on Friday November 13, 2026 @05:34PM
(#50491028)
Yeah, I think this is roughly where things are headed. And I think this is actually in the design of many languages already. This is made especially powerful by languages like Lean, as 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 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...