I've been experimenting with this a lot lately in Lean because it's equally capable as a theorem prover and as a programming language. It's resolving a lot of the frustration I feel with LLM coding.
You write a type signature for a function that amounts to "take a Foo x and return a Bar y with a proof of does_what_i_wanted(x,y)." Voila, no more agents doing something else because it won't compile if they don't do what I wanted.
It's great to build faster without the frustration of having no confidence in what I build. But it sure makes the gap between toys in Lean and using this in a Real Project in some other language that much more frustrating.
You write a type signature for a function that amounts to "take a Foo x and return a Bar y with a proof of does_what_i_wanted(x,y)." Voila, no more agents doing something else because it won't compile if they don't do what I wanted.
It's great to build faster without the frustration of having no confidence in what I build. But it sure makes the gap between toys in Lean and using this in a Real Project in some other language that much more frustrating.