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

41–50 of 63 posts

Re: Long division verified via Hoare logic

#41

Post by schoen »

groos wrote: post #36

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.

Apparently some aspects of Idris, Dafny, and (maybe) Isabelle are helping less-awesome logicians derive programs from their specifications nowadays.

(I haven't tried any of these languages so I don't have a personal story of how helpful they were for me.)

Re: Long division verified via Hoare logic

#42

Post by rikthevik »

groos wrote: post #36

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.

Sometimes I read a paper or see some code that makes me think that wizards are real and that they walk among us.

Re: Long division verified via Hoare logic

#43

Post by schoen »

puzzledobserver wrote: post #29
petschge wrote: post #21

Earlier quoted context omitted.

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…

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

Perhaps { int | _ >= x && _ >= y && (_ == x || _ == y) } ?

I just proved in Coq that if all of these always hold for a function, the function coincides exactly with the max function.

Re: Long division verified via Hoare logic

#44

Post by sjrd »

We actually proved correctness of the fast Long division of Scala.js using similar reasoning. [1] We had mechanical proofs for the other operations, but the solver couldn't handle division. The interplay between bit vector semantics and floating point semantics was too much for it to bear.

Scala.js has the fastest implementation of 64-bit integers on the JavaScript engine. The implementations cannot be understood unless you actually prove them correct. IMO that's one of the best reasons to invest in the formal proof of a program fragment.

[1] https://lampwww.epfl.ch/~doeraene/thesis/doeraene-thesis-201... section 4.4.2, page 114.

Re: Long division verified via Hoare logic

#45

Post by somat »

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…

I always wonder, how do you prove your proof is correct? is it turtles all the way down?

Another way to phrase it is, how do you prove your formal verification is verifying the correct thing? from one point of view a proof is a program that can verify the logic of another program. how do we know the one is any more correct than the other?

Re: Long division verified via Hoare logic

#46

Post by lmm »

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?

With dependent types, if you really want to. (Or just with conventional generics or typeclasses, the difference between a ring and a monoid will show, and that's enough for many cases).

Re: Long division verified via Hoare logic

#47

Post by robinhouston »

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.

Interesting to hear your experience. I was there 94–97, when the curriculum was still pretty heavy on formal methods (and functional programming).

For me it was wonderful. I already knew how to write computer programs, as that's what I had spent most of my waking hours doing before that point, but learning how to think rigorously about the correctness of programs was a revelation to me.

Re: Long division verified via Hoare logic

#48

Post by Joker_vD »

> Interestingly, it seems division by zero is impossible, because there is no suitable remainder.

Excercise: However, this algorithm still terminates and computes something, when provided with d == 0. What does it compute? Strengthen the postcondition with this information and adjust the proof accordingly.

Re: Long division verified via Hoare logic

#49

Post by maxidog »

chihuahua wrote: post #39
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 us…

Lol, thanks for that, was worried I was being too negative!

Re: Long division verified via Hoare logic

#50

Post by jlarcombe »

chihuahua wrote: post #39
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 us…

Not a single useful thing? A complete waste of time? Really not anything that you found intriguing or thought-provoking for its own sake? I did the same course nine years later and found it very stimulating, even if it wasn't always directly "applicable" so to speak. But perhaps the syllabus had changed a bit by then.
Post reply on HN