Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Loop invariants can give you coding superpowers

yourbasic.org

Post reply on HN
Print view View original

31–40 of 88 posts

Re: Loop invariants can give you coding superpowers

#31

Post by kyle-rb »

skrebbel wrote: post #12

I think there's an opportunity to name variables after their invariant. For example, in the typical sum example, the mutated variable is usually called "sum" or "total". But you could also call it sum_from_0_to_i, and then a reader can immediately see that the result is the full sum because i equals the array length. It's like a proof-by-variable-name. The same trick tends to work as well with less trivial invariants…

Why is 'totalUpToPrevious' better than 'sum' or 'total'? I could see it being good for explaining what a reduce does, but once you know how they work, 'sum' tells you exactly which argument is the accumulator.

Re: Loop invariants can give you coding superpowers

#32

Post by repler »

asark wrote: post #28

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…

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

Re: Loop invariants can give you coding superpowers

#33

Post by ConSeannery »

asark wrote: post #28

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…

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

Re: Loop invariants can give you coding superpowers

#34

Post by asark »

repler wrote: post #32
asark wrote: post #28

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…

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.

Re: Loop invariants can give you coding superpowers

#36

Post by mindslight »

asark wrote: post #28

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…

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

Re: Loop invariants can give you coding superpowers

#37

Post by Itaxpica »

GuiA wrote: post #10

The article describes the concept of a loop invariant and gives examples for a few algorithms, but unless I am missing something, it is not giving you any way to computationally verify those invariants? (I guess I am a bit surprised by the short length of this article because when I write code, I tend to think of it in those terms already, so I expected it to go further; but I guess not everyone has been exposed to t…

When we covered this in my CS 101 class back in the day, our professor actually had a system he had put together built on Python's unit testing infrastructure. Really, any construct in a programming language that lets you say "assert that this thing is true and if it isn't, do something" can be used for loop invariant checking.

Re: Loop invariants can give you coding superpowers

#38

Post by CuriousCosmic »

asark wrote: post #34
repler wrote: post #32

Earlier quoted context omitted.

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.

Re: Loop invariants can give you coding superpowers

#39

Post by Profan »

wsxcde wrote: post #13

If you're interested in playing around with loop invariants for non-trivial programs, I recommend the Dafny programming language which can automatically verify the invariants using SMT solvers. (Dafny is much more convenient that messing around with operational semantics in Coq.) There's a tutorial + web interface at: https://rise4fun.com/Dafny/tutorial/Guide . The official repository is here: https://github.com/Micr…

Yes!

Dafny puts this stuff front and center, it's all well and good to think about invariants, but if they're just expressed in a comment and not actually verified, they might as well be filler text!

If there's anything I hope the mainstream adopts at some point, it is some variation of what Dafny offers here.

Re: Loop invariants can give you coding superpowers

#40

Post by seagullz »

The following anecdote is from https://courses.csail.mit.edu/6.042/spring18/mcs.pdf:

The Invariant Principle was formulated by Robert W. Floyd at Carnegie Tech in 1967. (Carnegie Tech was renamed Carnegie-Mellon University the following year.) Floyd was already famous for work on the formal grammars that transformed the field of programming language parsing; that was how he got to be a professor even though he never got a Ph.D. (He had been admitted to a PhD program as a teenage prodigy, but flunked out and never went back.)

In that same year, Albert R. Meyer was appointed Assistant Professor in the Carnegie Tech Computer Science Department, where he first met Floyd. Floyd and Meyer were the only theoreticians in the department, and they were both delighted to talk about their shared interests. After just a few conversations, Floyd’s new junior colleague decided that Floyd was the smartest person he had ever met.

Naturally, one of the first things Floyd wanted to tell Meyer about was his new, as yet unpublished, Invariant Principle. Floyd explained the result to Meyer, and Meyer wondered (privately) how someone as brilliant as Floyd could be excited by such a trivial observation. Floyd had to show Meyer a bunch of examples before Meyer understood Floyd’s excitement — not at the truth of the utterly obvious Invariant Principle, but rather at the insight that such a simple method could be so widely and easily applied in verifying programs.

Post reply on HN