Hacker News Reader

Comment by asark | Hacker News Reader

To sum (haha) up, I am no n00b.

However, I've looked over the page a couple times and still can't figure out the use of this, let alone what "superpowers" it may grant. It's just comments? The best parts I can see are the mostly-prose ones farther down that just say what the loop's supposed to do, but even those are just repeating the "input" and "output" info, really, which are sort of also comments I think. Some of this might be useful if you could express it in types or some other machine-checkable fashion, but in comments they're just kind of redundant and, like any comments, must be treated with suspicion anyway.

What am I missing? I just have no idea what I'm looking at here, or rather I think I do but I'm entirely missing why it should be in any sense exciting which leads me to think maybe I don't.

View on HN

> be useful if you could express it in types or some other machine-checkable fashion

I think this is as close to the answer you can get in the paradigm in which you're asking. It is useful in the formal but non-machine-checkable realm to design the algorithm. Every invariant you can encode into the type system is a double win, but invariants you can't specify in the type system are still a win.

FWIW, direct exposure to abstract concepts like this is a benefit of a CS education. They're eminently learnable outside of a classroom (bottom-up), but you have to work to keep an open mind to recognize the trail of breadcrumbs that leads past your practicality-tailored preconceptions. Think of yourself as learning math, not programming.

You're not missing anything - it's 100/200 level computer science. (Freshman/Sophomore)

Yeah I'm just getting "if the loop can be expressed as induction you can... write that in a comment, for some reason". Alright, that's nice. Could we express that as tests instead plzkthx?

So I thought I must be missing something.

For the rare languages that support invariants (or has a library that implements invariants) you would write it as code rather than a comment and the compiler will compile time error if the compiled code is capable of violating the invariant.

Another place to use this is if you're designing a new bit of code and want to write the design out before you write the code, rather than code first (or as the code is being produced, where at times it's non-executable because you have holes in the program that are filled with these textual descriptions).

You could put some of these into asserts or similar. Like for the three way partition. Create an assert that at each iteration the array[:low] values are all less than p, array[high:] values are each greater than p, and array[low:mid] values are each equal to p. If it doesn't hold then you know your code is wrong. This does induce a performance hit, but asserts can be turned off for deployed code.

What the page presents is a tool for producing mathematical proofs. Proofs are really useful for mathematicians for with them you can derive lots of truths about mathematical objects. For example, it is true that if q^2 = 2, then q is not a rational number.

In the same way, using the tool on the page you can prove that 1. the while-loop terminates. 2. the invariants hold, meaning that your program is correct. Yes, you can encode the proof in a machine-checkable format but that is missing some of the point. Just like with mathematical proofs, the major use of the proof is to communicate with humans.

Also the same techniques used to prove invariants by hand can be used by compilers to implement smart optimizations. In the sum example, the compiler could deduce/prove that sum = \sum_{i=1}^n i and replace the loop body with n(n+1)/2. I don't know if any compilers do such advanced optimizations but theoretically they could (in trivial cases like these - in general, proving properties about code is as hard as solving the halting problem).

Other proof techniques involve finding upper and lower limits of variables which are used to store values in more efficient types. For example, storing an integer as an int32 instead of int64.

To really understand what's going on read https://en.wikipedia.org/wiki/Hoare_logic. The article's proof uses Hoare logic but implicitly, without the notation, so understanding how the proofs work is hard.

> using the tool on the page you can prove that 1. the while-loop terminates

Not quite. Proving that a while loop terminates is usually done by establishing a loop variant - intuitively, a claim that the inputs to the loop become "smaller" in some sense, i.e. closer to some exit condition/base case, with each iteration of the loop. Loop invariants don't suffice on their own.

I believe the superpower is the ability to prove correctness of the program easily.

For most of us, this isn't a big deal. But let's say you're writing a subroutine that will control part of a pacemaker, rocket, fighter jet, satellite- anything where bugs are deadly or expensive- then this is a Very Big Deal.

But this comment does not prove the program will execute correctly, or does it?

I've linked [1] to another example of exploiting an invariant that you might find more compelling. The presenter takes a multi-page mess of UI code from Chrome containing something like 8 loops, then solves an even harder version of that problem in ... 2 lines of code, by exploiting an invariant associated with the problem (and a well placed library call!).

[1] https://news.ycombinator.com/item?id=19567671

It's a badly written post. That's what you're missing.

In the first example, author didn't even indicate what the loop invariant is in the code, before moving on to a second example.

I'm right there with you, seems extremely routine.

Reply on news.ycombinator.com