SteveJS

I have several techniques queued up that attempt to counter it. The distinction in Agents.md is definitely part of it.

Not sure if they will work yet.

I am using lean as part of the prd.md description handed to a coding agent. The definitions in lean compile and mean exactly what I want them to say. The implementation i want to build is in rust.

HOWEVER … I hit something i now call a McLuhen vortex error: “When a tool, language, or abstraction smuggles in an implied purpose at odds with your intended goal.”

Using Lean implies to the coding agent ‘proven’ is a pervasive goal.

I want to use lean to be more articulate about the goal. Instead using lean smuggled in a difficult to remove implicit requirement that everything everywhere must be proven.

This was obvious because the definitions i made in lean imply the exact opposite of everything needs to be proven. When i use morphism i mean anything that is a morphism not only things proven to be morphisms.

A coding agent driven by an llm needs a huge amount of structure to use what the math says rather than take on the implications that because it is using a proof system therefore everything everywhere is better if proven.

The initial way i used lean poisoned the satisficing structure that unfolds during a coding pass.

Wife’s comment: “Cherries? It needs to be an apple.”

The larger project is to allow analyzing stories for developmental editing.

Back in June and August i wrote some llm assisted blog posts about a few of the experiments.

They are here: sjsteiner.substack.com

Also matryoshka and the ability to guide matches by using prefix instructions on the query.

I have ~50 million sentences from english project gutenberg novels embedded with this.

Having the llm write the spec/workunit from a conversation works well. Exploring a problem space with a (good) coding agent is fantastic.

However for complex projects IMO one must read what was written by the llm … every actual word.

When it ‘got away’ from me, in each case I left something in the llm written markdown that I should have removed.

99% “I can ask for that later” and 1% “that’s a good idea i hadn’t considered” might be the right ratio when reading an llm generated plan/spec/workunit.

Breaking work into single context passes … 50-60k tokens in sonnet 4.5 has had typically fantastic results for me.

My side project is using lean 4 and a carelessly left in ‘validate’ rather than ‘verify’ lead down a hilariously complicated path equivalent to matching an output against a known string.

I recovered, but it wasn’t obvious to me that was happening. I however would not be able to write lean proofs myself, so diagnosing the problem and fixing it is a small price to be able to mechanically verify part of my software is correct.

I do like the oddish (half cli / half tui) form factor of these ‘CLI’ coding agents. But i pretty much always pair with vscode for diff viewing.