Hacker News Reader

From a computer science point of view, it's the same argument as why NP-complete problems are hard to solve, and easy to check.

From a practical point of view, however, it's the same argument we write unit and integration tests. We accept error rates in the program under test, the test, the test harness, the programming language, the operating system, the hardware, and the universe. The goal is reduce the error rates enough you can ship something you can get paid for and won't get sued for later before you starve to death.

Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler.

Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith).

It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.

The problem with CompCert is that it produces really bad code, below the level of gcc -O0, about the level of the eternally-in-progress compiler project you worked on in your Programming Languages 370 course. So you can get most of the benefits of CompCert by running a standard compiler with -O0.

Nevertheless, this is a demonstration that verification can produced apparently bug-free code.

This is valid and my take is that domain modelling becomes extremely important in this context

More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket

One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with

And I think that's equally applicable to specs and business logic

Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.

LEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct.

In other words, proving something is essentially the same thing as type checking.

It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)

Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?

> Does Lean have a type for "list containing only prime powers"?

You can wrap a base type with a proof which is called bundling

inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n)

So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers

The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.

To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.

The difference is that (generally in programming languages) a type is something defined with a name while a constraint is ad-hoc. If you use types for everything you'll have to write a whole lot: this variable is a Size3List, this one is a Size5List, this one is a PrimePowersList.

Lean is a dsl for mathematicians, not computer programmers.

This is not remotely true, it was designed as a general purpose functional programming language and the adoption by mathematicians only came later with the creation of Mathlib.

It's not a DSL but has very powerful metaprogramming capabilities that make it great for creating DSLs

There's nothing the core language lacks compared to say Haskell

I wish DX was better for people not using VS. I have my opinions about tools and when trying lean out I got the impression that you basically have to use it. They also seemingly lack a REPL.

I also got the impression that they like sticking everything into Mathlib and not splitting off smaller packages that you could use as dependencies (besides Batteries).

Yeah I really dislike that you need neovim or VS to benefit from Infoview

Haven't tried it but there's this community-made REPL https://github.com/leanprover-community/repl

Using JSON as input and output of a REPL is certainly a choice.

Completely and 100% utterly wrong. LEAN is a functional programming language with a type system strong enough to express cutting-edge mathematics and proving it correct. And yes it also has DSL's built on top of it optimised for doing math but that is an extra.

>why would the formal verification be any more correct than the program it is verifying?

It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.

Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.

> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result

This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input.

Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.

The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc.

It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.

You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.

So for pedagogical purposes, can you tell us what you think the trivial spec is?

Trivial one: `forall i, j. 0 <= i < j < |sorted| -> sorted[i] <= sorted[j]`, which can be satisfied by copying a single element from `input` or by `sorted` being empty.

It can be fixed (feedback welcome) by adding: `forall i, j. 0 <= i < |sorted| -> |indexof_id(sorted, input[i])| = 1`, with `indexof_id` using equality by identity, which is crucial in practice.

Note that the amended definition implies quadratic runtime, which is the crucial difference between a specification and an efficient implementation.

you have the common problems with non-uniqueness and with extra elements. Your spec is met by:

    SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6

    SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6,7

and a bounds checking bug unique to your formal spec because you only check inputs up to the length of the output

    // first 0 elements of input must occur in output
    SORT(1,2,3,4,5,5,6) = empty list

    // first 6 elements of input must occur in output
    SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,7

My second condition would reject the additional element, as it would not be found in the input. have to be duplicated to However, I was lazy about the `|input| = |output|` constraints. With those constraints it would not be possible to omit elements from the input in the output.

Ok, I’ll bite, why is this wrong?

For a list of items I and an operator LEQ which returns bool for any pair of items in I, SORT() returns a list S such that:

1. Every item in I is present exactly once in S

2. For each consecutive pair of items (S_i, S_j) in S, LEQ(S_i, S_j) is true.

SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6

I'm sorry, do all 5's look the same to you!! /s

aka, one item in I is missing in your output.

No, if it had one more 5 it would violate your specification that every time must occur exactly once.

Also, SORT(1,2,3,4) = 1,2,3,4,7

Not my specification (drive by third party)

but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items.

> Also ...

Yeah, that needs tightening up by pastel8739

You need a way to differentiate the two 5s, that isn't present. If you had a list like:

  L = [(5,foo), (2,bar), (2,baz),...]

And did a:

  SORT(L, key=first) # or however it'd be specified

Then the duplicate 2s would be fine, because they're no longer duplicates, only duplicate keys. But it would still fail if (2,baz) showed up twice in the source and destination even though we've asked for SORT, not UNIQSORT.

In the cases of

  SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 ) and
  SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 )

one or both of those might be incorrect ?

( I'm teasing, perhaps )

More seriously,

> You need a way to differentiate the two 5s

As there's no unique filtering or other reduction going on here, there's a permutation chain from input to output.

But that's not in the specification given above. That specification is entirely wrong to specify SORT. It requires no duplicates survive the sorting process.

The specification said

    Every item in I is present exactly once in S

5 is an item in I, and it is present exactly once in S.

and 5 is another item in I, and it's not present in S.

Yes it is, it's right there, between the 4 and the 6.

That's not the same one - track the permutation chain.

What is the "same one"? Define item in "I" formally.

Are we talking about Values? Then inigyou is correct.

Memory locations? Then it is trivially true, but that does not prevent me from writing 0 into every memory location.

Value + Memory location? Then it does not work for arrays since we are modifying the memory locations by moving the values between them.

The abstract notion of manipulable things in a indexable order? You need to show how that correlates to reality in a way where you can not put in a hole even larger than this one you are trying to close.

To loop back, this very discussion shows how non-trivial it really is and how much thought actually needs to be put into handling even "trivial" problems. Almost everybody who talks about how we can replace these complex implementations with simpler, understandable specifications has little to no experience with the difficulties of actually creating correct specifications. Anybody who would bring up sorting as "trivial" either has no idea what they are talking about or is so far ahead that they have weird ideas as to what constitutes as "trivial". In both cases, their opinion is highly divorced from practical reality.

That is not to say that it is not worthwhile or even that the specifications are "more complex". It is quite possible the specification is still simpler despite the difficulty, but it is also likely the complex implementation was already totally incomprehensible and a simplified specification is also incomprehensible, it is now just formally incomprehensible.

The specification was extremely clear on this point. 5 is in the input, so 5 must be in the output exactly once. And 5 is in the input, so 5 must be in the output exactly once. It doesn't say anything about "tracking a permutation chain". Any output containing exactly two 5s violates the spec. You need a different spec because this one is clearly not what you intended, which is the point.

> I'm sorry, do all 5's look the same to you!! /s

You have that /s tag, but this is actually the problem with pastel8739's spec as written.

>> 1. Every item in I is present exactly once in S

This actually does require inigyou's example to be the result of calling SORT when you cannot distinguish repeated items from each other.

  SORT([1,1]) => [1,1]

The item 1 (which one? doesn't matter, they both do but we only need one to fail the post-condition to invalidate the result) in the source list has a count of 2 in the destination list, so this is an invalid result by the supplied spec.

pastel8739's spec also doesn't exclude the possibility of inserting new values (so long as they aren't duplicates of items in the source list).

1. The output is a permutation of the input.

2. If the comparison implements a strict total order, the output is sorted according to it.

You are correct.

However, that specification is not trivial. Almost nobody correctly articulates property 1 when first encountering the problem if they do not already know the answer or are already aware it is a trick question (and even then most software developers still fail).

Furthermore, that also sidesteps the problem of formally specifying what a permutation is. Unless you have a grab bag of already proven powerful theorems, the author is most likely also going to make a error doing that as well even if we start at a proof abstraction level comparable to normal programming.

Reality is that trivial problems admit trivially wrong specifications exceedingly easily. There is little reason to assume that much more complicated problems that are hard to even articulate will magically support obviously correct specifications that are simpler and more understandable than the code.

Note this doesn't make it useless, just not watertight. Proving that the output of a sort algorithm is a sorted list is genuinely useful and catches a lot of potential bugs. If your sort algorithm is "return []" you'll certainly notice that while writing the proof and fix it. It'll also be caught easily by any unit test.

It wouldn't catch all bugs - merge sort recursing on the same half of the list both times would return one item N times, which is sorted, and is a plausible enough mistake to make.

See how easy it is once you have right terms ;)

I think this works, but I could be proven wrong yet again.

You might also want to prove that the comparison implements a strict total order, but that would be part of the comparison's spec, not the sorting function's. There is another possibility for a mistake there: if you don't use exactly the same test, you might prove that your < implements a strict total order by its definition, while also proving it doesn't according to the sort function spec and thus allowing the sort to return anything.

Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.

The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.

do you have a reference to anywhere that discusses this further? It seems pretty trivial to me

Often the spec can be simpler than the original.

The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations.

The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.

Verification is sometimes less conceptually difficult than solving. I'd say for most well-defined problems, verifying is simpler.

E.g. finding a general solution for a cubic polynomial is difficult. Proving that a solution is correct is conceptually trivial: substitute a solution for x, and simplify. Many mathematical problems are well-defined in this way.

In the case of a compiler (CompCert), the program is already, in part, being written according to the language spec. So that definition can be used in verifying a compiler. In a domain where there is no standard specification or required properties, then coming up with a spec is hard (probably as hard as coming up with a solution).

> The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program.

It is a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.

Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs.

(It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)

> Rust has stated they do not intend to fix cve-rs.

Huh? That joke repo seemed to ride on https://github.com/rust-lang/rust/issues/25860 which is certainly considered a bug.

Here's an actually useful list of known soundness issues, all of which are bugs waiting to be fixed, no stupid snark needed: https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...