Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Long division verified via Hoare logic

cofault.com

Post reply on HN
Print view View original

21–30 of 63 posts

Re: Long division verified via Hoare logic

#21

Post by petschge »

nextos wrote: post #17
dwheeler wrote: post #16

Earlier quoted context omitted.

It's widely agreed that formal verification does not boost software productivity, in the sense that formal verification doesn't speed up development of "software that compiles and runs and we don't care if it's correct". The point of formal verification is to ensure that the software meets certain requirements with near certainty (subject to gamma radiation, tool failure, etc.). If mistakes aren't important, formal v…

Automation of Hoare logic is quite good these days. Dafny, from MS Research ( https://dafny.org ), is probably the most friendly formal language of any kind. It's built around Hoare logic and its extension, separation logic. The barrier of entry is low. A seasoned imperative or functional programmer can get going with Dafny in just a few days. Dafny has been used to verify large systems, including many components of…

How do you encode the difference between a method that adds and a method that multiplies two numbers in the type signature?

Re: Long division verified via Hoare logic

#22

Post by tristramb »

thaumasiotes wrote: post #14
unification_fan wrote: post #3

Earlier quoted context omitted.

Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stuff and it will actually work on the first try. You don't even need to write tests for it.

> What it does is guarantee correctness which is like the holy grail for programmers. Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.

It guarantees correctness relative to a given requirement.

The real value of formal proofs lies in forcing you to think deeply about the requirement and your implementation of it and to make your assumptions about it explicit.

I have only ever used proof once in my career. We had a problem with an aircraft main computer that it was occasionally failing during start up and then refusing start again on all subsequent restarts. It was a multiprocessor computer and each processor was running start up tests some of which would interfere if run at the same time. I was worried that if the start-up was stopped at an arbitrary time it might leave the control variables in a state that would prevent further start-ups. I used Leslie Lamport's first technique (https://lamport.azurewebsites.net/pubs/pubs.html#proving) in an attempt to prove that it would always start up no matter at what point it was stopped the previous run. But I was unable to complete the proof in one situation. So I added a time delay to the start-up of some of the processors to ensure that this situation never occured. But that didn't fix the original problem. That turned out to be a hardware register being read before it had settled down. I fixed that later.

Re: Long division verified via Hoare logic

#23

Post by 986aignan »

recursivedoubts wrote: post #9
ulrikrasmussen wrote: post #8

Earlier quoted context omitted.

Proving safety is just a small part of the problem to be solved. The hard part is actually structuring the program such that its correctness can even be formulated as a formal property which can be proved. For a lot of software that alone is highly nontrivial.

From "No Silver Bullet": > More seriously, even perfect program verification can only establish that a program meets its specification. The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification

On the other hand, proofs sometimes give you more than you'd expect. A proof that the implementation of a function always returns some value automatically proves that there's no arbitrary code execution, for instance.

Re: Long division verified via Hoare logic

#24

Post by hcarvalhoalves »

recursivedoubts wrote: post #2

i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…

Software has such huge economies of scale that, for the most part, being useful or cheaper than the alternative surpasses the need to be correct. Only for some categories of software being correct would be a priority or a selling point.

Re: Long division verified via Hoare logic

#25

Post by maxidog »

I studied “computation” at Oxford 92-95 while CAR Hoare was still there and basically all they taught us about computers were these formal methods. They actually thought it would revolutionise programming and looked down at anything else as “hand-waving”. Think the syllabus was abandoned only a few years later thank goodness.

Re: Long division verified via Hoare logic

#26

Post by CaptainNegative »

Not specific to this article, but it's tragic that computer science curricula, and discussions of these algorithms, virtually never highlight the tight connection between binary search and long division. Long division done in binary is exactly binary search for the correct quotient, with the number written above the line (plus some implicit zeros) being the best lower bound proven thus far. Similarly, division done in decimal is just "ten-ary" search.

Re: Long division verified via Hoare logic

#27

Post by schoen »

recursivedoubts wrote: post #2

i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…

My high school CS teacher in the 1990s had been influenced by this and told me that formal proofs of correctness (like with loop invariants, as here) were extremely tedious and that few people were willing to actually go through with them outside of a formal methods class.

This was a perennial topic of Dijkstra's as he complained about people writing programs without knowing why they worked, and, often, writing programs that would unexpectedly fail on some inputs.

But we're getting better tools nowadays. The type systems of recent languages already capture a lot of important behaviors, like nullability. If you can't convince the type checker that you've handled every input case, you probably do have a bug. That's already insight coming from formal methods and PL theory, even when you aren't thinking of yourself as writing down an explicit proof of this property.

I guess the compromise is that the more routine machine-assisted proofs that we're getting from mainstream language type checkers are ordinarily proofs of weaker specifications than Dijkstra would have preferred, so they rule out correspondingly narrower classes of bugs. But it's still an improvement in program correctness.

Re: Long division verified via Hoare logic

#28

Post by schoen »

LegionMammal978 wrote: post #20
rocqua wrote: post #18

Earlier quoted context omitted.

Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".

Taking the reductio ad absurdum, the program itself perfectly specifies its own behavior. Yet it's hardly something I'd point to as a holy grail. We want programs that do what we want them to, which is generally a human construct rather than a technical one. (And you'd better hope that two different people don't expect the program to do two different things in the same situation!)

Huh, this is kind of like other trivial objects in mathematics (typically the empty object and the universal object). One trivial property is "this program computes what this program computes" while the other trivial property is probably "this program computes something".

Although these are themselves only trivial in a programming language in which every string represents a valid program.

Re: Long division verified via Hoare logic

#29

Post by puzzledobserver »

petschge wrote: post #21
nextos wrote: post #17

Earlier quoted context omitted.

Automation of Hoare logic is quite good these days. Dafny, from MS Research ( https://dafny.org ), is probably the most friendly formal language of any kind. It's built around Hoare logic and its extension, separation logic. The barrier of entry is low. A seasoned imperative or functional programmer can get going with Dafny in just a few days. Dafny has been used to verify large systems, including many components of…

How do you encode the difference between a method that adds and a method that multiplies two numbers in the type signature?

If you ignore syntax and pretend that the following is a snippet of Java code, you can declare that a variable x always holds an int, like so:

var x: int = y + 5

Here x is the variable being defined, it is declared to hold values of type int, and its initial value is given by the term y + 5.

In many mainstream languages, types and terms live in distinct universes. One starts by asking whether types and terms are all that different. The first step in this direction of inquiry is what are called refinement types. With our imaginary syntax, you can write something like:

val x: { int | _ >= 0 } = y + 5

Once again, x is the variable being defined, it is declared to always hold a value of type int at all relevant instants in all executions, and that its initial value is given by the term y + 5. But we additionally promise that x will always hold a non-negative value, _ >= 0. For this to typecheck, the typechecker must somehow also confirm that y + 5 >= 0.

But anyway, we have added terms to the previously boring world of types. This allows you to do many things, like so:

val x: int = ... val y: int = ... val z: { int | _ >= x && _ >= y } = if x >= y then x else y

We not only declare that z is an integer, but also that it always holds a value that exceeds both x and y.

You asked for the type of a function that multiplies two numbers. The type would look weird, so let me show you an imaginary example of the type of a function that computes the maximum:

val f : (x : int) -> (y : int) -> { int | _ >= x && _ >= y } = ...

This doesn't really get you to the maximum, because f might be computing max(x, y) + 5, but it does show the idea.

The final step in this direction is what are called full-blown dependent types, where the line between types and terms is completely erased.

Re: Long division verified via Hoare logic

#30

Post by not2b »

LegionMammal978 wrote: post #20
rocqua wrote: post #18

Earlier quoted context omitted.

Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".

Taking the reductio ad absurdum, the program itself perfectly specifies its own behavior. Yet it's hardly something I'd point to as a holy grail. We want programs that do what we want them to, which is generally a human construct rather than a technical one. (And you'd better hope that two different people don't expect the program to do two different things in the same situation!)

There are other ways to exploit formal verification. For example, you may be able to formally prove that the unoptimized version of your program has the same behavior as the optimized version, subject to specified constraints. This can assure that there aren't any bugs in the optimization that affect program correctness. You're eliminating a class of bugs. Of course, it's possible that the unoptimized version is incorrect, but at least you can assure that your aggressive optimization approach didn't cause breakage. Such approaches are commonly used for hardware verification.
Post reply on HN