61–70 of 129 posts
Formal methods is like a plan. Everyone has one until they are punched in the face (real world requirements and trust boundaries).
Earlier quoted context omitted.
> 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 me…
>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()?
So when you write a function like:
func hypot(x, y):
return sqrt(x*x + y*y)
Earlier quoted context omitted.
>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()?
> 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…
Earlier quoted context omitted.
> 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 me…
> 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?
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
if x > 50:
x = 42
something_afterwards(x)
Earlier quoted context omitted.
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.
If you have an int32 or less you can!
Earlier quoted context omitted.
So, formal methods produce runnable systems, but communication remains the challenge. If a formal spec is messy, then it's a proof of ... what, exactly? A formal specification that bridges tech and product, that lets non-technical contributors read and discuss all the logical nuances, directly as operational code, at product's level of abstraction of interest, would transform a lot. It's no longer a challenge to crea…
The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the proof was 200K lines. Obviously human has to understand the spec deeply.
I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-…
... How do you know that the proofs are themselves correct?
Quis custodiet ipsos custodes?
The proof checker. You verify a proof system by having it produce a proof trace: - Step 3185: Apply rule that a * b = b * a to "length * width" in the current formula. Then you run a proof trace checker which applies each transformation in sequence and checks that the expected result is obtained. Provers are complicated, but proof trace checkers are really dumb.
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 t…