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.
(On a beefy machine) It gets 1 TB/s throughput including all IO and position mapping back to original text location. I used it to split project gutenberg novels. It does 20k+ novels in about 7 seconds.
Note it keeps all dialog together- which may not be what others want, but was what i wanted.
Here is a (3 month old) repo where i did something like that and all the tasks are checked into the linear git history — https://github.com/KnowSeams/KnowSeams
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.
It is not llm specific. A large swathe of it isn’t that much Microsoft specific either.
And it is a developer feature hidden from end users.
e.g. - In your ollama example, does the developer ask end users to install ollama? Does the dev redistribute ollama and keep it updated?
The ONNX format is pretty much a boring de-facto standard for ML model exchange. It is under the linux foundation.
The ONNX Runtime is a microsoft thing, but it is an MIT licensed runtime for cross language use and cross OS/HW platform deployment of ML models in the ONNX format.
That bit needs to support everything because Microsoft itself ships software on everything.(Mac/linux/iOS/Android/Windows.
The primary value claims for Windows ML (for a developer using it)—
This eliminates the need to:
Bundle execution providers for specific hardware vendors
Create separate app builds for different execution providers
Handle execution provider updates manually.
Since ‘EP’ is ultra-super-techno-jargon:
Here is what GPT-5 provides:
Intensional (what an EP is)
In ONNX Runtime, an Execution Provider (EP) is a pluggable backend that advertises which ops/kernels it can run and supplies the optimized implementations, memory allocators, and (optionally) graph rewrites for a specific target (CPU, CUDA/TensorRT, Core ML, OpenVINO, etc.). ONNX Runtime then partitions your model graph and assigns each partition to the highest-priority EP that claims it; anything unsupported falls back (by default) to the CPU EP.
Extensional (how you use them)
• You pick/priority-order EPs per session; ORT maps graph pieces accordingly and falls back as needed.
• Each EP has its own options (e.g., TensorRT workspace size, OpenVINO device string, QNN context cache).
• Common EPs: CPU, CUDA, TensorRT (NVIDIA), DirectML (Windows), Core ML (Apple), NNAPI (Android), OpenVINO (Intel), ROCm (AMD), QNN (Qualcomm).
Those are Jaz’s daily unique action counts (flows) from the Bluesky firehose; they’re anchored to the Nov ’24 spike, so the ‘decline’ is post-surge reversion. Meanwhile the user stock kept rising (~39M).
A presidential election spike is the baseline for tracking growth in a social media platform??
I zoomed out. It looks like this:
"Usage has absolutely declined from peak switching periods where inevitibly some users won't stick around, but that's to be expected"
That just isn't a "sharp decline" no matter how much you seem to want to repeat those words.
Personas are a great tool. IMO - By the time you arrived these had transformed into bad shorthand. (I say this having been in Devdiv through those years.)
Elvis is not a persona - it is an inside baseball argument to management. It suffered a form of Goodhart’s law … it is a useful tool so people phrase their arguments in that form to win a biz fight and then the tool degrades.
Alan Cooper, who created VB advocated personas. When used well they are great.
The most important insight is your own PoV may be flawed. The way a scientist provides value via software is different than how a firmware developer provides value.
Not sure if they will work yet.