Verification: code does what the specifications say

    Validation: specifications describe something we wanted to build

Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."

[1] https://en.wikipedia.org/wiki/Formal_verification

- Verification: Are we building the product right?

- Validation: Are we building the right product?

My intuition was different. To me verification is a process while validation is that the outcome of that process. As in: to validate the "+" operator, you verify that 1+2=3.

Looking at the Wikipedia article https://en.wikipedia.org/wiki/Verification_and_validation the definitions are not very clear and seem to depend on the context, tough the general idea is that of the LLM answer.

Funnily enough, the https://en.wikipedia.org/wiki/Engineering_validation_test Wikipedia article is introduced with "An engineering verification test (EVT)..."

It seems to be the kind of thing where everyone has a different idea and they are often conflated, making the distinction almost meaningless without context. You can give a precise definition for your project, but it may not apply elsewhere.

Note about using LLMs: I often like to use LLMs to settle these questions. Not because LLMs are flawless, far from it, but because they work by generalizing the content of their training dataset, they should do a pretty good job on extracting consensus. It fact, it is all they do; when a LLM tells the truth, as it is often the case, it is because the consensus is often the truth.

AI verification: AI meticulously abuses all available loopholes to deliver answer expected by operator, rather than actually responding to the problem.

Simplest example: proof that `x+1 > x` (borderline impossible)

The description was most likely given in a natural language, with many assumptions about the shared objective reality.

Today, we have LLMs, which de facto (but with significant flaws) formalize the interpretation of natural language, as well as the shared objective reality we inhabit. They are becoming closer to the truth than any individual human. (Their construction is a wittgensteinian program of sorts.)

So we can take an LLM with the prompt "Respond according to the following specification:" plus the original specification/requirement, in natural language, itself, as a program A.

Then we can take the written program itself, together with the emulator of the machine it runs on, as a program B.

We can feed both of these into some theorem prover - and formally prove that program A and program B give identical outputs on identical inputs. That's most likely the best we can do, ever.

(Or we can, in theory, develop programs this way, as a solution to the following question: Which program, when run on the given platform, gives provably identical answers to program A? That's a general program synthesis problem.)

In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.

A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].

[1]: https://prela-lang.org/

[2]: https://github.com/remysucre/prela/tree/sqlstorm

[3]: https://github.com/remysucre/prela/tree/doom/

How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts

pgrust is incredible btw

Dude, this is a database.

Concurrency is the source of all the hard stuff in databases.

Databases without concurrency are super-trivial.

I don't see any fundamental limitation that would prevent this from scaling up further.

The fact that you've dodged all the hard stuff is a pretty fundamental limitation.

I feel like a good chunk of my skills that I honed over decades as a software engineer are obsolete: programming, debugging, navigating code. But there are other skills and especially experiences that, at least with the current level of tools, allow me to do much more than someone who doesn't have them: knowing what computers can and cannot do, or only inefficiently; distributed systems; deployment; CI/CD pipelines.

I find it unrealistic anyway, that market will be saturated so fast, it won't make a difference for you or me, in the grand scheme of things.

It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.

It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.

The bonus here is that you can cut in at the prose spec stage and change it to whatever you need, as well as being able to target it at specific technical choices at the last couple of steps.

Where I've seen this work really well is with privilege escalation management, where you do actually want to be careful about the states the system can get into, and the APIs available for managing privileges in a system might be super specific to that system. But I can imagine the workflow being quite a useful one any time you've got anything state-machine flavoured.

Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.

A while back a knowledgeable man was a philosopher, and they could all easily talk to each other and understand. As time went we split up - we have philosophy doctors in various fields who have very little to talk about.

This happened again when the term “engineer” fractured (even before software engineering). Software engineering itself fractured, too.

And it’s happening again now.

Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.

You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.

However just like the uptake in SaaS, iPaaS, serverless, managed cloud environments, this means way smaller teams will be needed, and everyone that doesn't get to press buttons at the software factory, will need to find another occupation.

This result is exactly the opposite. They're verifying at the machine code level, which is totally imperative.

I think for now the answer to adaerlangsql+++ is just Rust - but its semantics have always been about human usability.

Humans have this thing where we can only keep 7 things at once and have to juggle our context, but recall seems much more broad than model contexts.

If we were to start designing a language and toolkit based around LLM context sizes, limitations and quirks - how would that look?

Also terseness and operators are one thing, but what if it’s the other way around - English words etc - can have a much bigger vocabulary of things that can be done but can easily be generated on the fly.

For a new LLM language realistically you would need to probably either write or convert a shit ton of software to it first if you are to train an adequate model on top of it …

And also what about “IDEs” for agents? So far they are clumsily using human tools - just looking Claude string along bash loops and greps to try to eek out meaning form code _it itself had written a week ago_ is frankly frustrating.

There must be a better way and some rich agent specific tooling for code exploration and verification.

Anthropic stance has always been “yeah we tested them all, grep is better” but I still am not convinced - just by the fact that it constantly fails one or two attempts before “figuring it out” yeah it’s fast anyway but it could be _faster_ and could allow the agent to “think” in code space more and not have to validate itself at every minute step …

I’m generally cautious/sceptical about the current LLM hype, but if that did ever happen and it worked to a useful degree, it might truly be a significant advance. I’m not saying that just because of the LLMs themselves, though.

To reach that point, we would first need to overcome the classic problems in this area:

1. How can you specify the required behaviour for a system in precise detail without ending up with a specification language that is essentially another programming language with similar complexity to the ones we use today?

2. How do you solve the sufficiently smart compiler problem so that producing reasonably efficient and reliable implementations of those declarative specifications is not only viable but expected?

And then, if you still need someone (let’s call them a “developer”) to carefully specify the required behaviour of the system in detail, and you also know how to reliably generate a good implementation of a specification, how much value is left for LLMs to add in this picture?

Maybe LLMs really could be trained to reliably produce good implementations in that scenario? Never say never, but it seems more likely to me that we would develop deterministic algorithms for doing so. That’s already a very hard problem that a lot of smart people have explored, but if a solution could be found, most likely it would be strictly better than relying on LLMs in this part of the process.

Maybe there would still be a role for LLMs to convert natural language problem statements into specifications? Maybe for systems that don’t really matter, that would be enough and a big time saver. However, I’m sceptical about how much time it would be likely to save for systems that did need to work, where you would still need careful design and review of all the detailed specifications by developers anyway.

Maybe LLMs would end up in a similar role to the scaffolding tools that are popular in some ecosystems today, where you feed in some basic choices and the tool then produces a first pass at the files and code you might need, which you take as a starting point for the real work but without wasting so much time on boilerplate? That seems realistic and useful, but it’s a relatively small part of what would then be the overall development process.

In short, I would love for the existence of LLMs/agents to push us towards those better programming languages and tool chains, but if that did ever happen, I wonder how much benefit LLMs/agents could still offer once developers had the more powerful languages and tools available and could work at a “higher level of abstraction” themselves.

Linus doesn't have to care, MirageOS already exists for OCaml, and I'm pretty sure there's something like MirageOS for Rust...

This was to be expected, llms are trained on a very large corpus of data, they 'look' like creative from our point of view, as humans don't have that much knowledge, so, if the LLM proposes something that a human does not know, it looks like creative. But they stay neural networks after all, so very good in interpolation, very bad at extrapolation. Building new knowledge is extrapolation if it's truly outside the convex hull how the dataset.

I usually write code and ideas that are at the border of the convex hull, I haven't seen yet an llm being able to propose a really innovative solution. All the time they reuse building blocks that are already there. And I really tried pushing by making them creating proofs.

If I have an insight on some problem and I ask for the proof for it, it will usually be able to generate the proof, but that proof is never creative, and often it will use novel ideas only if I explain the novel idea. It will not come up with it alone. (And sometimes it's very hard to even explain the ideas, as it tends to return to knew waters)

Its only a data point, but I haven't seen a paper that handle this issue yet, and I don't expect them to magically become good at extrapolation due to the theory behind neural networks.

Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.

If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.

So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning

[0] https://creusot.rs/

[1] https://flux-rs.github.io/

[2] https://lean-lang.org/use-cases/aeneas/

> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.

> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.

- - -

This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.

If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.

It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.

One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.

I love that “convex hull” analogy. LLMs can certainly serve as a channel for knowledge transfer. They can help spread knowledge and know-how throughout society, enabling breakthroughs that were simply held back by practical limitations (e.g. lack of money, time, or expertise). Personally, I think LLM is more valuable as a tool for democratizing knowledge than as artificial intelligence.

I mean, even just that would prove to be a very productive workhorse - potentially being able to automate away almost every white collar job.

This is not just plausible but in fact the most likely result.

We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.

But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.

But when you stop doing that, they choke on their own spaghetti.

It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.

> Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.

However, you're correct that this is not formal verification in the sense of a correctness proof against a full specification validated to capture what the program is intended to do. Pretty impressive though.

What they did is tried to prove that the conventional fuzzer won't find crashes. Where they found counterexamples, they fixed the bug and tried again.

In essence, a fuzzer takes random samples out of a space of possible inputs that could crash. They proved that nothing in the space of possible inputs could crash.

This is a strictly more powerful result than a fuzzer could give you.

It's absolutely cool to see this sort of validation process get cheaper and easier, but it means nothing if no one cares enough to do it. EAL1 certification can be as cheap as a beefy server, but it's not commonly done because effectively no one cares.

As microsoft learned with the zune just because it's cheaper or better at the same price doesn't mean anyone will use it. Culturally, we have to make the effort of verifying code worth it.

[1]: https://en.wikipedia.org/wiki/Rainbow_Series

Preferably, I wouldn’t trust my life to a calculating device running on AA batteries while dangling from a rope.

So why do people work? For the vast majority of people there are three main incentives:

1. Survival. You need food and shelter. Most people don't own anything so have to do whatever the owners want them to do to meet basic needs,

2. We get satisfaction from helping, pleasing and impressing other people,

3. We get personal satisfaction from doing a good job, being proud of our outputs and learning and honing our skills.

A bad job like factory work or unskilled labour only has incentive 1. Nobody takes pride in how well they've cleaned a toilet, nor does anyone appreciate it. Better jobs get 2 and 3 as well. We generally got all three incentives in abundance.

What we're seeing is the loss of incentive 3 and inevitable eventual loss of 2. Those were what drove us to do more than the bare minimum that's required for 1. That's why we would spend time thinking through things, struggling with problems, learning and bettering ourselves in the process. Now there's no personal satisfaction because an LLM could do it. And we know that there's nothing really stopping other people doing to too, so what we did soon won't even be impressive or help others (although we can cling on to it for a little while maybe).

We have a few options going forward. On a personal level we could try searching for something that gives us the satisfaction we once had, or we could just accept that we'll become wage slaves likes so many others. On a societal level we could all decide to minimise the amount of work we do, given that it's much less enjoyable now.

You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.

Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.

You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.

At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.

For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.

If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.

Most software is ultimately like this

I think learning to code will still help with the other things here - its a good first step, even if its now obsolete on a direct level. Like how its useful for mathematicians to be able to calculate by hand even though calculators exist - it gives intuition for how to operate the tools and check results

2017: Leslie Lamport: Video course on TLA+ (328 points, 74 comments) https://news.ycombinator.com/item?id=13918648 (219 points, 2018, 17 comments) https://news.ycombinator.com/item?id=16956778

2017: Writing correct lock-free and distributed stateful systems in Rust, with TLA+ (374 points, 94 comments) https://news.ycombinator.com/item?id=14373359

2019: TLA+ model checking made symbolic (197 points, 51 comments) https://news.ycombinator.com/item?id=21662484

2019: Introduction to TLA+ Model Checking in the Command Line (176 points, 44 comments) https://news.ycombinator.com/item?id=18937214

2019: Learn TLA+ (387 points, 92 comments) https://news.ycombinator.com/item?id=19661329 (310 points, 2020, 58 comments) https://news.ycombinator.com/item?id=22393653 (254 points, 2022, 64 comments) https://news.ycombinator.com/item?id=33010645 (350 points, 2022, 75 comments) https://news.ycombinator.com/item?id=31952643

2020: Using TLA+ in the Real World to Understand a Glibc Bug (166 points, 76 comments) https://news.ycombinator.com/item?id=24958504

2026: Hunting a 16-year-old SQLite WAL bug with TLA+ (239 points, 29 comments) https://news.ycombinator.com/item?id=48730953

...

https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

no idea what you are even talking about

They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.

See for yourself:

https://github.com/Giancarlos/Culebral

Anyway, my custom (currently paused because I'm taking on a much more ambitious compiler project with Claude... just to push the limits) language can build ASP .NET applications, and a bunch other things. I also took the Rust approach to types, all method signatures must have types defined, type hints are inferred when declaring new values from the value on the right.

I've also had Claude rewrite legacy C# projects with 100k+ lines of code, fully in Rust, long before Opus 5.0. I've spent the last year pushing the limits with Claude, including reimplementing existing software, which people are catching on to now, and I've managed to get rather far in some cases.

So I wouldn't be surprised if yes, Claude can implement Python, mind you, there's Python interpreter coded in Python in what was it? 500 lines of Python? You can build a Python stack machine bytecode interpreter in like 60 ~ 80 lines of Python code.

Would not surprise me if you can trim a C programming language interpreter down in terms of lines of code when you rewrite it in Rust especially when you have access to a much more functional language, not to mention Rust took the best bits out of OCaml it could to make itself very efficient at writing compilers / languages (so they could write their own compiler in Rust...).

I am also having Claude building me a much smaller compiler, which started out in under 500 lines of Python, but as I got more ambitious it had to write more code for my language, it was meant to be a slightly less restrictive Go, the Python basically converts the syntax to C which then compiles anywhere. Havent put that one on GitHub since I'm still tinkering with it.

And like yes, it does just launder defects to a layer higher, but another way to phrase that in this case (and in many other cases) is that it raises the bar.

Instead of defects being mostly about nonsense minutia (relative to business logic), they are about actual design decisions and their correspondence to reality, i.e. the actual original goal and point of this god forsaken, navel-gazing field.

I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.

Proving two things are equivalent is a major component of formal.

For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.

A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.

Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."