Long division verified via Hoare logic
51–60 of 63 posts
Re: Long division verified via Hoare logic
#52We 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 unl…
> The implementations cannot be understood unless you actually prove them correct
I quickly scanned the book you provided, but I couldn't find an explanation.
What do you mean by 'understood'?
Re: Long division verified via Hoare logic
#53I 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…
Just a heads up.
> I followed this up with Ph.D. in Computer Science somewhere else, which was also a complete waste of time.
It has been shown this form of thinking results in depression.
Re: Long division verified via Hoare logic
#54Earlier quoted context omitted.
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.
What I learned from these comments sharing their experiences from one time to another is that the curriculum evolved and no one had the same experience.
Not to mention how individuals perceive things - two students with similar aptitude in the same class can still have their own very different experiences.
Re: Long division verified via Hoare logic
#55i 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?
Because a proof verifier has a fixed complexity, regardless of the proofs it needs to check. Also, a minimal proof verifier is of almost trivial complexity. More advanced and performant verifiers can bootstrap from the minimal one by provably reducing to it.
Re: Long division verified via Hoare logic
#56Earlier 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!)
The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted" postcondition. The code OTOH could be arbitrarely complex.
Re: Long division verified via Hoare logic
#57Not 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 i…
[deleted]
Re: Long division verified via Hoare logic
#58Not 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 i…
Very cool observation, I never thought of that. Thanks!
Re: Long division verified via Hoare logic
#59i 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…
> will likely not be a major boost for software productivity
You can make plastic knives much faster and cheaper than metal ones. Production!
Re: Long division verified via Hoare logic
#60Earlier quoted context omitted.
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!)
The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted" postcondition. The code OTOH could be arbitrarely complex.
To be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".