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