4 ms·

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

• jlebar 4mo ago
  > 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 4mo ago
    >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 4mo ago
      > 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.
      • pydry 4mo ago
        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 4mo ago
          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 4mo ago
            It's also possible it's not the future of programming.
            • chadgpt3 4mo ago
              It never was. It's useful but extremely slow.
      • brap 4mo ago
        This makes a lot of sense, thank you!
      • 4mo ago
    • deleted 4mo ago
      [deleted]
    • chadgpt3 4mo ago
      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____ 4mo ago
        > 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 4mo ago
          > 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____ 4mo ago
            Unicode never ceases to amaze me.
    • nemo1618 4mo ago
      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____ 4mo ago
        Exactly. You can prove that f(a,b) always returns a+b. And then you overflow the int on that machine. Oops.
        • codebje 4mo ago
          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.
  • parthdesai 4mo ago
    > 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?
    • Jtsummers 4mo ago
      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.
    • Agingcoder 4mo ago
      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.
    • akoboldfrying 4mo ago
      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 4mo ago
  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.
• jaggederest 4mo ago
  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.
• comonoid 4mo ago
  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 4mo ago
    If you have an int32 or less you can!
    • jaggederest 4mo ago
      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 4mo ago
  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.
• chadgpt3 4mo ago
  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.
• jcranmer 4mo ago
  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 4mo ago
    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.
• mhh__ 4mo ago
  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
• majormajor 4mo ago
  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?
• rendaw 4mo ago
  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.