Long-form arguments on programming languages, correctness, and the parts of software engineering that resist automation.
// The industry's default answer to insecure AI-generated code is more AI: an LLM checker hunting for bugs an LLM wrote. Fighting fire with fire only ever secures the common case — this traces a path to baking security into generation itself.
→// AI code generation is really a specification problem — and a spectrum of tests, types, and formal methods that narrow the guess.
→// Invariant inference, execution oracles, and the limits of pure AI audits: how a "poor man's neurosymbolic" loop forces LLMs to write down their assumptions, then fuzzes the assumptions themselves.
→// Every breakthrough technology starts as a faster version of the old thing. The true paradigm shift comes when you abandon the old constraints entirely. Are we there yet with AI and software?
→// Agentic orchestration layers are turning software maintenance from a brittle, depreciating asset into a fluid, self-optimizing substrate — replacing the engines of a commercial airliner mid-flight.
→// Test suites aren't enough. CCC passed all of them, then shipped 19 silent miscompilations. FastRender deadlocked under real CSS. The fix: replace sparse test signals with formal invariants agents cannot argue past.
→// When AI agents treat code as a temporary resource — generated, executed, and discarded — human-readable source files become unnecessary overhead. But removing them triggers a process dependency cascade: every engineering practice built on source code must be rebuilt on agentic primitives.
→// As agentic code generation explodes, we are hitting an unyielding complexity ceiling. The mandate of this epoch is not to rebuild the familiar slightly faster, but to abandon procedural scripting for intent-driven, formally verified systems.
→// Zero-day discovery has become a commodity, delegated increasingly to autonomous agent teams. The defensive literature answers with a four-pillar stack — harden, watch, contain, patch — but the feedback arrows between the pillars are where the architecture goes quiet.
→// Across the US, UK, and China, AI funding is hollowing out foundational computer science. The UK is the purest case: centralized, ring-fenced, and suffocated by a 212% personnel-cost hyper-inflation that core systems cannot survive.
→// Grammar-constrained decoding makes it mathematically impossible for a model to emit invalid syntax. That guarantee cuts both ways — closing off failure modes nobody could patch before, while quietly deleting the model's ability to say no.
→// Thirty years after cypherpunks printed encryption code in paper books, history is repeating itself in AI. The boundary of national security regulation has moved from cryptographic algorithms to model weights — and the same enforcement dilemma is back.
→// Enterprise security bet on one frontier model doing everything until the latency spiral caught up with it. The literature's answer is dozens of small, disposable, locally-abliterated models orchestrated by deterministic code — cheap enough to run on every request, narrow enough to audit.
→// J.P. Morgan says AI has collapsed the vulnerability-to-exploit window from a year to a day. It's right about the machine-speed side — and its own footnotes concede the breach data showing 98.6% of disclosed CVEs never get exploited at all.
→// McKinsey's 2023 framework for measuring individual developer productivity triggered the same rebuttal software engineering has delivered every decade since 1968 — and GenAI tooling is now failing the identical way, one layer up, measured in tokens instead of lines.
→// Why consensus correctness is blockchain's actual product, what “correct” formally means, and the four distinct ways a formal-verification claim can fail even when the proof itself is real.
→// Lean 4's real paradigm shift for interactive proving, the Mysticeti case study's LLM-co-authored provenance, and the Aeneas/Charon code-extraction gap. Five recent protocol case studies close on the verdict — whether any of it actually reaches production.
→// AI coding agents have made it cheap to write a second blockchain client from scratch — real projects (rustock, ETH2030, XVI/Guillotine, SHiNode) prove it. What they haven't fixed is N-Version Programming's fifty-year-old asterisk: majority voting only masks bugs that fail independently, and the evidence on AI ensembles says they mostly don't.
→// Agents keep finding the gap defenses left open — Hugging Face, the Irregular disclosures, UK AISI, Astra. Five frameworks — AWS Dogwood, NVIDIA NeMo Guardrails, Cloudflare WriteGuard, Niels Provos's IronCurtain, and NVIDIA OpenShell — answer by pushing authorization out of the model and onto a deterministic proxy (or the kernel itself) at the tool-call boundary, checked framework by framework against their own announcements.
→// What the deterministic chokepoint doesn't close: permission creep, the audit-ledger and latency costs none of the five frameworks advertise, and the academic literature the novelty framing skips past. The verdict.
→// When autonomous agents can discover and weaponize zero-day vulnerabilities for pennies, reactive patching collapses. The only survivable architecture enforces structural runtime invariants — making it physically impossible for a vulnerability to execute a destructive action.
→// Frontier LLMs wired into symbolic tooling are finding weaknesses in real cryptographic schemes, not by inverting ciphertext directly, but by driving the tools that can. Anthropic's HAWK and AES results took a week to discover and a month to verify; that ratio, not the work-factor drop, is the actual headline.
→// 2025–2026 produced real agentic-swarm cyber incidents, each documented by its own disclosure — GTG-1002, JadePuffer, the OpenAI–Hugging Face breach, DseWiki. The threat-intel genre treats them as one phenomenon; the primary sources split cleanly into two structurally different failure modes.
→// Agentic LLMs have collapsed the cost of cloning software toward zero, from a $50,000 SaaS product rebuilt over a weekend to Google's own engineers reporting LLMs authoring most of a 39-migration effort. What hasn't collapsed is proving a clone is behaviorally correct, and that gap is reshaping software IP, security, and architecture all at once.
draft// As AI compresses the time from disclosure to working exploit, the patch-window math every security team relies on stops holding — and the harder problem turns out to be the human pipeline behind it, not a single super-attacker model.
draft// LLMs have turned code porting from a brittle, rule-based transpiler problem into generative "software recreation." The catch is in the benchmarks: code that passes every unit test while getting 5.6x slower, and AI-assisted commits that introduce 1.5x more security vulnerabilities than they fix.
draft// DARPA's TRACTOR program and four neuro-symbolic pipelines — C2SAFERRUST, SACTOR, VERT, &inator — promise to close the gap between mechanical transpilers and raw LLM synthesis. The catch: pass rates scoped to code that survived the pipeline, and proofs bounded to a fixed number of steps, not unbounded ones.
draft// Post-textual software strips out human-readable source so agents can target the raw hardware. Code golf has been simulating that world for twenty years — golfers trade names, structure, and comments to save a byte, and the golfing languages, the tricks, and the benchmarks are the closest working preview of the software nobody will ever read.
draft