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

31–40 of 63 posts

Re: Long division verified via Hoare logic

#31

Post by thaumasiotes »

tristramb wrote: post #22
thaumasiotes wrote: post #14

Earlier quoted context omitted.

> 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 r…

> It guarantees correctness relative to a given requirement.

OK, but given that you don't know what that requirement is, how does that help you?

Re: Long division verified via Hoare logic

#32

Post by jlarcombe »

maxidog wrote: post #25

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.

Still a strong presence in 98-01 but also lots of functional programming, algorithms and complexity and the tail end of the parallel research boom. I loved it.

Re: Long division verified via Hoare logic

#33

Post by ted_dunning »

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?

It is hard to understand what you mean by type signature, but I think what you mean is something like the type signature in Java, Go or C.

That isn't what people are talking about when they talk about formal verification with a type system. They are talking about much more complex type systems that have equivalent power and expressivity to formal logic.

This intro is good at introducing the topic. Unfortunately, the correspondence between advanced type systems and logic is itself fairly abstract and uses lots of concepts in non-intuitive ways. This means that you can easily wind up in a situation where you can do lots of proofs about number theory using a tool like Lean4, but you don't really see the corresponding types (this is what happened to me).

https://leanprover-community.github.io/learn.html

Re: Long division verified via Hoare logic

#34

Post by ted_dunning »

thaumasiotes wrote: post #31
tristramb wrote: post #22

Earlier quoted context omitted.

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 r…

> It guarantees correctness relative to a given requirement. OK, but given that you don't know what that requirement is, how does that help you?

But you do know the specification, or at least parts of it in many cases.

In the upstream example, one specification is that some reasonable time after you turn on the airplane, the flight controller is ready to fly. That's a very reasonable spec and important to verify in the given story. It is a thin end of the wedge for a lot of real-time guarantees that you might like to make.

As another instance where the specification is known, what is the specification of compiled object code? The specification of compiled code is the source code and proving that the object code matches the source code is a way to protect against adversarial tool chains. Check out seL4 for an example of this kind of formal verification.

Memory safety is another property susceptible to formal verification. The Rust community is making use of this very nicely.

The net lesson is that even if it is impossible to get formal specifications for lots of things, there are lots of other things where you can define good specifications (and you might be able to prove you meet them, too!).

Re: Long division verified via Hoare logic

#35

Post by ted_dunning »

AnimalMuppet wrote: post #13
unification_fan wrote: post #11

Earlier quoted context omitted.

But you don't have to do the proving. You can let someone who is, like, REALLY good at formal verification do it and then benefit from the libraries they produce Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.

Same problem. Sure, it would be great if the primitives we use were proven correct. But I've got stuff to write today, and it doesn't look like the proven-correct primitives are going to arrive any time soon. If I wait for them, I'm going to be waiting a long time, with my software not getting written.

The memory safety of the Rust standard library is an example of something where formal methods are bearing fruit already.

So you don't necessarily have to wait.

Re: Long division verified via Hoare logic

#36

Post by groos »

A couple of decades ago, I attended a lecture by Tony Hoare about program correctness. He used the producer-consumer problem as an example and by starting with pre/post conditions and refining them, he arrived at a (proved) correct program. I went back from the lecture thinking this is so easy, I can apply this as well. Sadly, I realized one has to be Tony Hoare to produce code out of logic with his level of ease.

Re: Long division verified via Hoare logic

#37

Post by e2021 »

rocqua wrote: post #18
thaumasiotes wrote: post #14

Earlier quoted context omitted.

> 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.

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

how do you know the specification is correct? Its turtles all the way down here

Re: Long division verified via Hoare logic

#38

Post by fooker »

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?

Basically weird type systems that encode pre/post conditions.

These ideas have not caught on for a reason. You end up writing the logic twice, and pretty high chances you mess up once.

Re: Long division verified via Hoare logic

#39

Post by chihuahua »

maxidog wrote: post #25

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.

I studied "Mathematics and Computation" there in 89-92 because they seemed to think that "computation" was a fad that was probably going away, so you couldn't let people study just "Computation".

There was a certain amount of formal methods, but only in a perfunctory manner, as if to satisfy an inconvenient requirement. Some functional programming, but in an extremely shallow way. Overall, I did not learn a single useful thing in 3 years.

I followed this up with Ph.D. in Computer Science somewhere else, which was also a complete waste of time.

Re: Long division verified via Hoare logic

#40

Post by vacuity »

schoen wrote: post #27
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 progr…

My algorithms professor says Dijkstra was wrong about most things, but I think many of Dijkstra's opinions are justified or right. But certainly it wasn't the right time for many of his remarks.
Post reply on HN