Long division verified via Hoare logic

Neat. Division being iterative makes me feel better about last week when I couldn't think up a good closed-form solution for something and I didn't feel like computing gradients so I just made a coordinate descent loop. It'll be funny if it's still in there when it ships

I realized this in school but it was beaten out of me because making a wrong guess in the process was unacceptable.

Very cool observation, I never thought of that. Thanks!

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.

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.

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.

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

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

> 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'?

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.

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 verification is a terrible tool. If mistakes matter, then formal verification may be what you need.

What this and other articles show is that doing formal verification by hand is completely impractical. For formal verification to be practical at all, it must be supported by tools that can automate a great deal of it.

The need for automation isn't new in computing. Practically no one writes machine code directly, we write in higher-level languages, or rarely assembly languages, and use automated tools to generate the final code. It's been harder to create practical tools for formal verification, but clearly automation is a minimum requirement.

True, but also the work can be reduced significantly with better tooling, which is still being developed but has improved markedly over the past decade. Eg SMT solvers that can output proofs, or tactics in Coq or Lean.

I'm hoping that this will be a big application of AI actually. If an AI can be built do to this simple but very tedious work, and your verification tool is capable of catching any errors it makes, then you've covered up a major flaw of formal verification (its tediousness) and of AI (its tendency to output bullshit).

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.

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?

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.

> will likely not be a major boost for software productivity

You can make plastic knives much faster and cheaper than metal ones. Production!