However, I think there is a middle ground between the "naturally verifiable" and the difficult cases. Certain domains, like banking apps, can want correctness guarantees about UI behaviour. A closed-off app can be very normative, so in theory specs like "the user did this action and confirmed it" can be made meaningful. But tying specs to UI is a tricky thing, and it's clearly volatile in a way function boundaries are not - apps go through redesigns, styles and elements move, etc. The abstraction of a UI as a state machine isn't hard to imagine, but actually hooking a spec into the program is a problem unto itself, and the common response is to simply ignore these problematic domains and do something easier like a backend spec that doesn't have to deal with the questions that aren't PL-shaped.

Secondly, I think the open partial specs, composable specs would help address the problems with monolithic specs that Dodd's cites. https://muratbuffalo.blogspot.com/2026/08/composition-and-mo...

A huge part of my goal is to write a "spec" of the format. I want it to be good enough that users can legitimately file bugs against my primary implementation for not following the spec: it is the source of truth about the language.

So, of course, I find it really interesting to discuss the grey space of "shrug, maybe this is correct". This whole process has been driving me to (a) make the language itself resilient and permissive so that it has _some_ answer for nearly all documents and (b) to constrain the output of the system such that it throws away as much information as possible, enabling us to make claims about semantics more confidently.

I don't know if I'm going to succeed at all my goals. This is sort of a small project and definitely far simpler than, say, a web browser. At the same time, it's very hard to narrow in on what it is, really, that I want such a spec to say.

I use model checking (a form of formal methods) daily. I separate the process into three domains: things that must be fully specified, things that can be fully specified, and things that, with the appropriate mitigation, need only have certain properties verified. Most software fits just fine in the latter category. Spend your time on fully verifying process isolation, cryptography, certain core runtime functions / behaviors, and logic relating to authentication and authorization. Everything else can be partially verified, which is much easier. Verify termination, no UB, memory safety, and that function contracts, data structure invariants, and API boundaries are followed.

A PDF implementation, a web browser, or a random server application fits cleanly into this decomposition. It matters little if the PDF is rendered oddly, or if the web browser can't interpret a page. But, it matters greatly if these errors could result in a vulnerability that could be exploited, or to a lesser extent, if these errors resulted in the software crashing.

Pure formal methods is academic. Apply engineering to this, and you get a real world and practical framework for making software safer.

I keep thinking about various ways of “pushing back” on an agent, shortening feedback loop and extending what we can grantee about results.

At the most low level we can nullify probability of the next token if that token is not desirable (eg json schema enforcement under constrained inference), this is the fastest pushback. Various compiler checks, linters, unit tests, exotic type systems, e2e tests, production traces. Wondering what else is out there.

On a tangent, iirc pascal allowed single-pass compilation, so I wonder if we can embed compiler directly into inference, sort of constrained inference on steroids.