9 posts
Cleanroom verification requires generating and discharging proof obligations.
Cleanroom software engineering demands that you prove your code correct before you compile it. That sounds noble until you spend three hours writing loop…
I spent 30 days writing design explanations before asking an LLM for code. The results changed how I think about rubber-ducking.
Most developers use LLMs backwards. We describe what we want in five words, get 200 lines of code back, and spend the next hour debugging assumptions the model…
LLM conversations contain intent, rejected alternatives, and working code. That's exactly what documentation should be.
You spent forty-five minutes with Claude designing a retry circuit. You explained the failure modes, rejected exponential backoff because it hides cascading…
Fagan inspections need four to six people and two hours to review 250 lines.
A full Fagan inspection needs a moderator, a reader, two to four inspectors, and the author. The team spends two hours reviewing roughly 250 lines of code at…
Large language models write surprisingly good Rust, but when you ask them for a formal proof they hallucinate invariants and invent syntax that no verifier...
LLMs can write Rust that compiles and even passes . What they cannot do reliably is write a formal proof that the code is correct for all possible inputs. The…
LLMs hallucinate syntax because they sample tokens probabilistically.
Ask an LLM to generate a JSON object and it will eventually emit a trailing comma, an unescaped newline inside a string, or a bare word where a quoted key…
You can generate design tokens from plain English descriptions, but only if you treat the description as a bounded-context DSL with a schema contract and...
Yes, you can describe a theme in English and get a working design system. The catch is that the English description is not a prompt. It is a source file. And…
Running multiple LLMs in parallel catches errors that any single model will confidently ship.
You ship a prompt to GPT-4o. It returns a JSON blob with a confidence of 0.97. You ship the same prompt to Claude 3.5 Sonnet. It returns a different JSON blob,…
N-version programming with LLMs doesn't require multiple models.
N-version programming assumes diversity comes from different authors. With LLMs, that means different models, different providers, maybe different training…