[brap]

Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”.

I guess doing things twice can help catch errors, but I fail to see what’s so special about formal specs if they can suffer from the exact same bugs as the tests/implementation.

I guess the root of the problem is if you want to formally prove that a program does something, you have to be very specific (heh) about what that something is, at which point you are basically just writing tests/implementation all over again.

I have been looking into this on and off for years now, and I keep feeling like I’m missing something, but I don’t know what it is.

Can anyone enlighten me?

[jcranmer]

There's a famous quote from Dijkstra: "Program testing can be used to show the presence of bugs, but never to show their absence." The flaw of testing is that it can only test the behaviors that you think might be problematic. To actually reach into the category of proactively fixing behaviors that you didn't know could go wrong, you have to reach for more exotic tools in the toolkit. Fuzz testing is a start down this path; formal verification is a different start down this path.

Obviously, the quality of these sorts of tools is dependent on your ability to write a formal model that is comprehensive in allowing behavior you want to be acceptable and disallowing behavior you want to be unacceptable, and we're still surprisingly far from that in many fields.

[pfdietz]

The problem with that mindset is that testing, like verification, becomes extremely powerful as it becomes more automated and you throw more compute at it. And it's arguably easier to automate testing than it is to automate formal verification.

Sure, testing isn't perfect. But is finding 100% of the bugs that much better than finding (say) 99% of them? This is especially the case if the missed bugs tend to be those that happen very rarely.

A formal specification allows automatic generation of tests. So run billions of tests, randomly generated, and see if any violate the specification.

Even theorem proving systems use this sort of thing as a short cut, for example pruning off attempts to prove a universally quantified statement by looking for counterexamples.

[jlebar]

> Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. [...] Can anyone enlighten me?

A big difference is that formal methods allow you to use the "for all" quantifier.

For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace".

But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace".

This is a trivial example, but you could imagine something more complicated, such as "for any program P, compile(P) has the same behavior as P".

Of course, you have to define what "has the same behavior as" means!

[brap]

>Of course, you have to define what "has the same behavior as" means

And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no?

In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

[bluGill]

> In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can go on and on. There's a huge number of different sorts that computer science have discovered over the years. They all should have the same result and so you should be able to prove they do the same thing. However, in the real world there are often reasons you would prefer one to another despite all meeting the same spec.

[gsnedders]

Another obvious example are cryptographic hash functions: if you have a function f(s) = h, you can trivially specify a function inverse_f(h) = s st f(s) = h, and if you can infer a non-brute-force algorithm for that, you’ve just inferred a cryptographical weakness!

[pydry]

I did some of this stuff in college and what bugged me was that the spec actually ended up more complex than the code and it had bugs.

That was a long time ago and they said that formal methods were the future back then, too.

[chadgpt3]

It's possible for that to happen but probably means either the function is too trivial or you're missing some abstraction in the spec

[pydry]

It's also possible it's not the future of programming.

[brap]

This makes a lot of sense, thank you!

[nemo1618]

I think the key is that, while you may think you have a full formal spec of f(), you actually do not. You have a program written in some language, and that language has its own spec, and the language is compiled to asm which has its own spec, and the asm executes on an architecture that has its own spec, and so on.

So when you write a function like:

  func hypot(x, y):
    return sqrt(x*x + y*y)

You might think you have "fully specified" hypot, but this is far from true! You have said nothing about what registers will be used, for example. This is not a problem; quite the opposite. It's the whole point of using high-level languages: they let you focus on what you care about. A spec is just a program in a very-high-level language.

[____tom____]

Exactly.

You can prove that f(a,b) always returns a+b.

And then you overflow the int on that machine.

Oops.

[codebje]

I am not sure that the perspective you have taken is the same as what I understood from the parent post; what I took from it is that things like registers, memory locations, ways to implement square root, and so on, are all _implementation choices_ that are not important properties of the specification. You specify that the hypotenuse is the square root of the sum of squares, but whether square root is implemented using Newtonian approximation or a fast inverse square root is irrelevant; whether your first argument is passed in a register or on the stack is irrelevant.

Often, things like resource usage are not specified: running time, memory consumption, etc, aren't relevant enough to appear in a behavioural specification.

If your spec says "f(a, b) returns a + b", but it's just a high-level document you can use to help guide your implementation, integer overflow is just one of many ways your implementation might be inconsistent with the specification. It's still likely that the existence of a formal specification you reference during implementation means that more edge cases have been considered ahead of time than if you just had an informal spec.

If, on the other hand, you prove it but it turns out not to be true (ie, you overflow integers), your proof is wrong. If a machine verified your proof and gave you a big thumbs up, your machine verification is wrong.

If, in Idris, I write "f : (a : Nat) -> (b : Nat) -> (c : Nat * c = a + b)", then I cannot compile an implementation for which I can't show a proof that the result is _always_ the addition of a and b, for all a and b, unbounded by anything but the resources at hand with which to run the program. An implementation subject to integer overflow won't compile.

Or, I could write "f : (a : Bits32) -> (b : Bits32) -> (c : Bits32 * c = a + b)" and implement something where , but then modulo arithmetic on overflow is _part of the specification_, because "+" in there is doing the heavy lifting of being defined as addition modulo 2*32 already; by specification, 4 billion plus 4 billion is ~3.7 billion.

[____tom____]

Perhaps I have misunderstood or was unclear.

Everything the parent comment mentioned were implementation details that did not affect the correctness of the code.

I just wanted to point out that there are implementation details that DO affect the correctness of the code.

And, of course programs need to run on multiple architectures. So it's hard to do what people seemed to be talking about in this thread and verify code just from the source code.

If you have the luxury of proving the correctness of the CPU, compiler and OS, that should be a big win. Otherwise, it seems to just be another type of testing. Still useful, but calling it verified or proven seems a bit much.

From my perspective, it seems more to be writing another, more complicated program, with more opportunities for bugs, and seeing if the results agree

[Joker_vD]

Well, ideally you proof should've failed because your axioms should be aware that arithmetic operators in the programming language of your choice are operating modulo some large power of two, and thus don't produce correct results for some particular inputs.

Admittedly, this one peeves a lot. Remember when Java's binary search and mergesort (and implementations in many other languages' standard libraries) turned out to have a bug of this kind [0]? Admittedly, the proof was informal, but if you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are, right? The integers do overflow in Java, that's explicitly stated in the Java's spec... and that means that a lot of even the most simplistic code has some very non-obvious correctness preconditions, which most of the times, I believe, are simply hoped to be true.

[0] https://research.google/blog/extra-extra-read-all-about-it-n...

[chadgpt3]

Non trailing whitespace means the string doesn't end with a space. But foo is a function that converts an AST to a string, that's totally different. Or it's a function that loops until \0 and changes all spaces to +

The spec should be a summary of what the impl is supposed to do. You'd want more than just doesn't end with whitespace of course.

[____tom____]

> Non trailing whitespace means the string doesn't end with a space

No. And this is a great example of the problems with specifications. You still have to write a spec. And this, too, is subject to bugs.

What's wrong with the statement above is there are 17 space characters in Unicode and another eight whitespace characters, like newline.

If you try to verify that something ends in whitespace, you have to make sure you have the right definition.

Not picking on parent poster! It's just a great example of the fact that you can verify, but if what you are verifying is wrong, it doesn't help.

[Joker_vD]

> there are 17 space characters in Unicode and another eight whitespace characters, like newline.

And of course, those 25 characters don't include ZERO WIDTH {SPACE,NON-JOINER,JOINER,NON-BREAKING SPACE} and WORD JOINER, which gives you yet another 5 arguably "it's kinda space, right" codepoints which definitely should not be trailing in any reasonable text string.

[____tom____]

Unicode never ceases to amaze me.

[parthdesai]

> But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace".

Isn't that essentially property testing?

[Agingcoder]

Formal methods allow you to prove that it works for all inputs, and not just for the small subset that will be sampled by property testing

It’s a proof, not a successful experiment.

[Jtsummers]

Property testing is stochastic, which may be fine, but only gives you a statistically (hopefully) high chance of discovering a problem. If you use something like SPARK/Ada, you can actually embed a proof in the code so that you actually know that the code is correct (for what you've proven). PBT scales better than embedding proofs, though, and is highly effective in practice along with fuzzing.

[akoboldfrying]

Unless you literally try every possible combination of inputs (which is usually infeasible), property testing can't give you mathematical guarantees about correctness. You can think of it as a halfway house between classic testing and formal verification:

Classic testing: A human comes up with some concrete example inputs for which they know the "right answers" (corresponding outputs). They write code that runs the code under test, gets its actual outputs, and compares them to the desired outputs.

Property testing: A human comes up with a precise way of randomly generating concrete example (input, desired output) pairs. They write some code to describe how to generate the pairs, often using a declarative DSL that describes only constraints on the inputs and outputs, with the understanding that anything not expressly forbidden is permitted, like "The input can be any list of between 0 and 100 integers each between -500 and 500" and "Every integer in the input must appear the same number of times in the output". They then write some more code (often a single line) to ask the computer to use this "spec" to randomly generate, say, 1000 such pairs, or as many pairs as can be checked in 1s. The computer generates the pairs itself, runs the code under test on each input and and checks its output matches the desired output.

Formal verification: A human comes up with a spec that typically describes conditions that must hold for all (input, output) pairs. This may look very similar to, or even exactly like the DSL used for property testing, though in general there are other conditions that can be expressed that cannot be checked with property testing even in principle -- for example, checking that the program always eventually terminates. The main difference is that the code under test is never actually run; instead, the computer analyses the source code itself to attempt mathematically prove that the stated conditions hold. How to actually accomplish this is a field of active research, but one basic approach is called "symbolic execution". To greatly simplify, if we forget about loops and conditionals for a moment, the idea is that we can write down things we know must be true after each statement executes, based on the things we knew must be true before it executed. So for example if x is a variable initially containing any integer (and we ignore overflow) then after the line

    x = x * x

runs, we know that x >= 0. To handle conditionals like

    if x > 50:
      x = 42

    something_afterwards(x)

the prover "forks" into two cases: One in which we know for certain that x > 50, one in which we know for certain that x <= 50. At the end of the if statement it then has the task of recombining what is known about the two cases. In this example, the first case lets us conclude that x = 42 by the end, while the second case lets us conclude that x <= 50 by the end, so it could conclude that x <= 50 either way by the time execution reaches something_afterwards(x). Handling loops is trickier but generally involves looking for invariants.

[y1n0]

I don’t write software, but in asic and fpga design, formal method specifications enable the use of things like SAT solvers to determine if the underlying test article meets the specification.

You specify properties of the design and the tooling tests the design in a variety of ways to see if it can violate those properties.

Let’s say you have a system that controls turn signals. You can specify properties that say things like lanes that cross each other can’t both have a green light at the same time or even within some period of time of each other.

The tooling can exhaustively check the design for this and surface code traces that violate it.

[majormajor]

The powerful difference is between specific testing and exhaustive proving. If you fail to think of a test for an edge case, whoops. If you have a good model, you can know that it exists—and fix it—before you ship.

This is particularly valuable IMO in concurrent/distributed/multi-threaded situations where race-conditions and deadlocks are extremely hard to test and reason about. "Can A, B, C happen in the order 'A, C, B'" types of things.

I have a rough hypothesis that maturity in this space looks something like:

1) LLMs will allow much faster learning and usage of formal methods, even if initially just for "do it a second time" post-hoc verification

2) From there you move towards automation of LLM-checking "hey, the implementation code changed, does it look like it broke the model" - though this is still not deterministic, but it's likely a lot better than a human review requirement of something that only changed infrequently would've been

3) And then the real jump will be taking tooling for "write just the formal spec, let the implementation get generated" to the next level. There's various mostly-not-fully-baked-for-what-most-companies-would-want projects already out there for codegen like this, what if the LLM tools can accelerate the year-or-two of manual work it would take to make one of them fit your needs?

[jaggederest]

It's more than just "write the same tests just in a different way", because each test is largely independent, or grows to unmanageably large, and you have to do the work of figuring out the completeness of your test suite by e.g. branch coverage or other relatively crude overlap methods.

Statically proven type systems let you do this in a way that each contributing piece is checked in advance against all the other pieces, guaranteeing not just "this test passes" but, in combination, "all these tests create a reasonable, coherent whole", and it disallows incoherent models from being implemented in the code. An example of this is like Rust's match, which requires complete coverage of all the possible branches, but writ large across an entire codebase.

You're right that it does nothing for you if you make a fundamental logic or theory error, it can't catch that kind of error, but you'd be surprised how much more robust it is than "merely" e.g. Haskell's type system + ad hoc functional testing + property testing - which I would consider a quite strong system overall, but formally proven e.g. cryptography is a much higher bar.

[mhh__]

Lamport phrases this as "Thinking doesn't guarantee we will be right; not thinking guarantees we will be wrong" - specifications are for reasoning about systems in the deepest sense

[comonoid]

The book "Program = Proof" by Samuel Mimram starts with a formula which is true for all n below

n = 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889

I don't think you can catch it with any test suite.

[pdhborges]

If you have an int32 or less you can!

[jaggederest]

And you'll rapidly return to proofs when your "function input" is something like a sequence of, say, ieee floating point numbers coming over the wire of possibly unbounded length. State machines with proofs that all the cases are handled are great.

[IshKebab]

That can definitely be a problem, and I have definitely written formal specs (for hardware in SVA) where I'm like "I'm just implementing this again". And actually that's a totally valid formal verification task to do - formal equivalence checking of an implementation against a model (which is just another implementation). I can feel (and sometimes is) tautological.

However you usually try to not do that. If possible (and it usually is possible) your formal spec will be either:

1. Another implementation, but a much simpler one. For example you can formally verify the equivalence of a pipelined dual issue CPU, with a combinatorial single cycle model.

2. More general properties that much be true about the implemention, rather than exactly what the implementation must be. The classic example is compression: decompress(compress(x)) == x.

[rendaw]

The same with unit tests, they're best suited for problems where the specification is much simpler than the implementation. A sorting algorithm can be long and complicated, but a unit test just needs to present unordered input and assert that the output matches ordered output. A sorting algorithm is also well suited for formal verification.

If you're rewriting the implementation, I think it's probably not a good use for unit tests or formal verification.

As another commenter said, unlike unit tests which cover a specific case, and where you need multiple tests for edge cases and both positive and negative results, formal verification will cover all cases.

[chadgpt3]

For trivial functions they can be. Function: isPrime. Impl: loop to sqrt(n) and check divisibility. Spec: returns true if nothing divides. Impl: return true at the end if we didn't return false.

It's not exactly the same because your spec says nothing divides, not just up to sqrt(n). It's definitely not a test if you do it right.