whoke

I like the concept of "inevitable grittiness"! I think languages like Lean actually do a very nice job of pushing the grittiness out to the boundaries of your program. Everything else can stay pure, and in domains that are amenable to mathematical reasoning (compilers, DSP, etc) it feels like a natural fit. I don't think you have to go all in, either. I ported the compiler project I'm working on from TypeScript to Lean and recently spent a weekend making all the functions total and implementing a few basic theorems. On a basic level it feels like writing Haskell, but there's a lot more room to grow with it.

I'd say this is relative to the novelty of the problem domain. At work I'm often solving problems that have fairly standard solutions, e.g. Python scripts to automate build and execution workflows. For this stuff I'm often happy to delegate architecture, and in general, since I spend a lot of time working with legacy code, the solutions the models develop are both clearer and more maintainable than what was already there. The personal project I'm working on (small research compiler for stateless computation) has sparse precedent, and because of this I spend a lot more time hashing out architectural questions with the models. I think of it as a collaborative enterprise.

"you haven’t done any of the hard thinking you would normally do in writing the code yourself"

It's true, I spend less time solving problems that arise naturally from the process of implementation. But implementation errors have a poor signal-to-noise ratio. For every error that exposes a real design problem there are 10 others that involve routine fixes: type errors, scope issues, import resolution, dependencies. There's a common argument I see being thrown around, which is "how will junior engineers develop into senior engineers if they don't get reps in with implementation?" But to me it feels like "programmer" and "architect" are becoming more and more orthogonal as the models improve in capability. If my goal is to be an architect, getting more reps in as an architect is in my best interest, and letting the agents do the dirty work frees up space for me to spend the mental effort where it counts. And anecdotally, the scope of projects I've started taking on has scaled roughly linearly relative to how much work I'm able to delegate, while the mental engagement has stayed constant.

I think the interesting part here is that the black box gives us a starting point. And it's not a true black box: if a model is generating Lean, we can examine the entire source, iteratively refine by refactoring into smaller self-contained units, and the compiler gives us the certainty that our decomposition is correct.