Specifications Don't Exist (2025) | Hacker News Reader

Specifications Don't Exist (2025)

galois.com

59 pointssurprisetalk13 comments

A very valid take on spec writing. It sometimes feels like the research on formal verification is like the drunkard searching under the lamppost, in that the target is often a domain which is itself well-suited to a particular kind of computer science being done on it.

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.

There are now projects like Specula that, using LLMs, enable us to derive specifications from the implementation, and somewhat paradoxically, use those specifications to find bugs in the implementation. https://muratbuffalo.blogspot.com/2026/08/specula-scaling-fo...

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...

I've been spending the last couple months working on a Markdown-like lightweight document format. (Short pitch, it's like Markdown but with natural extension points built in and far less subtlety).

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.

This article comes close to making a fallacious argument about formal methods, which is that formal methods aren't useful unless you can exactly specify how something works.

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’m not just being funny, but how do you define undefined behavior?

You can define what constitutes undefined behavior without defining the behavior itself. Programming language definitions rely on this. So “verifying no UB” means verifying that a program is not performing any operations that have undefined behavior. Simple example: dereferencing an uninitialized pointer.

I get that, but I meant more philosophically, why is it especially useful to verify that no behavior is undefined if the defined behavior is also not defined, other that according to the compiler spec?

I may be missing what you're asking. To extend the example I gave, it's very useful to be able to verify that a program never dereferences an uninitialized pointer. In general, it's very useful to be able to verify that a program doesn't do anything that could cause UB.

That’s fair I suppose I’m being a bit obtuse.

But this level of formal verification gets you to the level of confidence you’d have if you had written the program in Rust or Java in the first place. The original post was talking about formally verifying what the system does as a whole, not just verifying the absence of a certain class of errors. I’m not questioning the value of eliminating null pointer dereferences that do exist, just the value of holding a formal proof of the absence of null pointer dereferences in a certain piece of code, given that there are many other possible bugs that that code could contain.

I mean, if I had a formal proof that my banking system could never double-spend money, that could be a useful property that someone would want to know about the system. If I have a proof that my banking system never dereferences a null pointer, there’s not very much I can be sure of on the basis of such a proof.

The difference is that Rust and Java can only verify certain properties. I can build model checks to verify any property that I can discharge with an SMT solver, which is significantly more powerful. For instance, I can build function contracts that verify that if a function succeeds, it performs certain actions, and if it fails, it does not. I can verify that a function properly manages external resources, performs authorization checks, or always follows data structure invariants.

I don't need to build full formal specifications to do this. I can verify just the subset that is important. I can do more than what Rust or Java provides. I can add more rules that must be followed, or in cases where it doesn't matter, I can relax specific rules without reaching for clumsy annotations like "unsafe", or using an FFI.

Yeah again fair enough. You can use formal methods to provably maintain invariants that are useful to you in development without shipping formal proofs of full system behavior.

Do you find that given a formal spec an agent can write complete implementation you don’t have to even read?

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.

I think that reading and reviewing software is responsible.

Source code exists for humans to read first, and for computers to read second. Programming languages are unambiguous, and most languages take well to abstraction. Software can be written at a level that is appropriate for human review. Boilerplate can be avoided. It's well written when it is easy for stake holders to understand directly, without translation and without an LLM to summarize it.

Software should be the output artifact of the process, because it exactly describes the behavior of the system. The formal specification explains how the software embodiment must work, and in constructive proofs, it's even possible to extract the software embodiment from this specification. But, from a practical perspective, this is too time consuming. Instead, specification should be written to explain the rules that software must follow, instead of the exact behavior. In this case, the source code is still an important artifact, and it should be reviewed and improved upon as part of the process.

Reply on news.ycombinator.com