> Looking it up, I think I did that when I was 16, but I've never used it while programming.

Any reasoning about loops or recursion requires an implicit understanding of proof by induction. Making it formally explicit seems like a perfectly fine idea.

In some sorts of code, you can get a lot of mileage from "loop invariants" and "loop variants". Understanding these is more or less the same as understanding proof by induction.

Whether you are missing anything depends on whether you ever write the sort of code that benefits from this. (Even if you do, you still might not be missing anything. You might be comfortable with loop invariants but not have connected them with proof by induction. Or you might be good at reasoning about these things in other ways that don't involve invariants.)

(You can stop reading here if you're already very familiar with loop variants and invariants.)

Here's the sort of thing I mean by loop variants/invariants. Suppose you're writing a binary search. (Don't write a binary search. Use someone else's that's already had the bugs taken out.) This is basically pretty simple but surprisingly easy to get subtly wrong, which means it's the sort of code it may be useful to write and document in such a way that you have an informal proof of its correctness. Like this:

  function find(a, x):
    # find x in sorted array a; return index i such that a[i]==x
    # or -1 if no such index exists. Takes time at most
    # proportional to log(#elements).
    lo,hi = a.index_bounds()
    while lo<hi:
      # INVARIANT: min index <= lo < hi <= max index+1
      # INVARIANT: if x is in the array then lo <= its index < hi
      # VARIANT: D := hi-lo reduces to at most D/2 next iteration
      mid = lo + floor((hi-lo)/2) # may equal lo, can't equal hi
      if a[mid] == x: return mid # done!
      if a[mid] < x:
        lo = mid+1
      else:
        hi = mid
      # INVARIANT: if x is in the array then lo <= its index < hi
    # now lo >= hi which means there's nowhere for x to live
    return -1

The above is pseudocode in no particular language. Is it correct? Those variants and invariants (1) divide that question in two and (2) provide a strategy for answering the second half of the question. First sub-question: if the (in)variants always hold, does that imply that the code is correct? Second sub-question: do they always hold? (Strategy for second sub-question: proof by induction on array size and/or number of iterations.)

The first invariant implies that since mid is always between lo (inclusive) and hi (exclusive) it's safe to access a[mid]. The second, given that it holds at both start and end of the loop body, implies that if we exit the loop then indeed x isn't in the array. The only ways to leave the function are via the return in the middle, which only happens when we have explicitly found x, and via the return at the end, which only happens when x is known to be absent; therefore, if we return anything, we return the right thing. And the variant says that the quantity D, which starts by equalling the number of elements in the array, is reduced by a factor of at least 2 at each step; as it's always a (strictly) positive integer, this implies that the number of steps is at most log_2(n), so the function does return.

(Note that that last bit is more or less a proof by induction on array size that the function always returns.)

So if the invariants hold then the function does the right thing in the right amount of time.

Proving that the invariants hold is the induction-like bit. The first invariant holds at the start (since lo,hi start out being exactly min index and max index + 1). Each time around the loop we replace either lo or hi with something in between the two, so we still have min <= lo <= hi < max+1; and we will exit the loop unless in fact lo<hi. So the first invariant always holds.

The second invariant holds at the start (since lo,hi are bounds on the entire array). Because the array is sorted, our adjustments to lo/hi make this invariant true again for the next time around the loop. So the second invariant holds at the end of the loop -- and of course therefore at the start of the next iteration.

(Note that those were both proofs by induction, though I wasn't super-explicit about the fact.)

The variant works because if we write D = hi-lo and E = floor(D/2) then the new value of D is, depending on which branch of that if we take, either E or D-E-1; note that D-E-1<=E; so new-D <= E <= D/2 as claimed.

It's probably pretty clear what sort of code this is useful for: highly "algorithmic" code that's basically doing something fairly simple but that's tricky to think about and easy to get wrong. If you're writing a language's standard library, or implementing some sort of iterative mathematical algorithm, then you're quite likely to find it useful. The less like that your code is, the less often this technique will be useful to you. (Fairly extreme example: if you are writing a CRUD webapp then it is unlikely that anything you do will benefit from this.)

(Slightly off topic, but maybe still interesting.) I used to write binary searches like yours, with two tests per iteration:

    while lo < hi:
        mid = (lo + hi) // 2 
        if a[mid] == x:
            return mid
        elif a[mid] < x:
            lo = mid + 1
        else:
            hi = mid
    return -1

But then I discovered that there's an alternative approach which has only one test per iteration:

    while lo < hi:
        mid = (lo + hi) // 2
        if a[mid] < x:
            lo = mid + 1
        else:
            hi = mid
    if lo < len(a) and a[lo] == x:
        return lo
    else:
        return -1

If comparisons are expensive compared to other operations then this is twice as fast as the variant with two comparisons per iteration. (If comparisons are cheap, as they are if you are searching an array of numbers in a compiled language, then it doesn't make much difference.)

Anybody interested in invariants for reasoning about correctness of loops/data structures, CMU has a good set of intro lecture notes here https://www.cs.cmu.edu/~rjsimmon/15122-s16/schedule.html

I'm afraid you're not very good at explaining yourself, I've no idea what point you're trying to make.

Sorry to burst your bubble, but any moderately complex LOB CRUD app usually has a large amount of far more complex algos than a binary sort. Your off-hand comment shows a total ignorance of what's involved in writing a LOB CRUD web app.

In my experience, algos are the really easy part of programming. The hard part is managing complexity.

> In my experience, algos are the really easy part of programming.

His point is that when you design an algorithm you need to be able to reason about why it works.

Based on the rest of your comments in this thread, it sounds to me like you have something against the mathematical background of CS? Writing code is not the same thing as doing computer science. Plenty of people are perfectly happy doing the former, but CS as an academic discipline is rooted in discrete math so any school that teaches it should also teach the background.

Ah, the old "but it's not a programming degree, it's about theory". I thought we were past that these days.

Notice how it took you just one sentence to summarise the few hundred words he wrote.

We've a fairly big problem in this industry that "qualified" CS graduates don't actually signal anything about their suitability for the profession. A significant chunk can't even fizzbuzz.

I'd suggest teaching mathematical models instead of showing loops and recursion in practical code is a large chunk of the problem.

> it took you one sentence to summarise the few hundred words he wrote.

Oh, come on. What sornaensis's one sentence summarizes is ... the one sentence at the start of my comment. It's true that his is shorter; it also gives less information.

(For the avoidance of doubt, that isn't a problem. Since you declared yourself unable to understand what I wrote, it's fair enough to try to simplify it.)

The rest of what I wrote was (1) an answer to your subsidiary question "What am I missing?" plus (2) an explanation of what I was talking about, in case it was stuff you weren't familiar with.

(Of course if I'd known you'd respond as unpleasantly as you did, I wouldn't have bothered trying to be helpful. But at the time I thought you might well be asking a sincere question rather than just wanting to vent about how out of touch those hoity-toity theoreticians are.)

I don't know how you came to the conclusion that the quality of CS graduates is poor or how that the cause of this perceived lack of quality is somehow due to courses focusing on theory. In my experience very little in a run of the mill CS undergrad program is dedicated to theory so I might come to the opposite conclusion: too many people are focused on learning how to write code with some javascript framework and not how to do computer science. So people miss important patterns and concepts because no one explained to them why they are important. Patterns you have spent years coming to understand intuitively, perhaps.

(It looks like you've been downvoted a lot. For what it's worth, it wasn't me.)

I didn't claim that CRUD apps don't have complexity in them. I claimed that CRUD apps don't typically have the sort of thing in them for which this kind of small-scale semi-formal stuff is useful in them. I am happy to stand by that claim; do you actually disagree with it?

I get the impression that you think I was being sniffy about CRUD apps. I wasn't. In particular, (1) I don't think CRUD apps are low-value. There are plenty of CRUD apps that add much more value to the world than almost any piece of code of the sort that invariants are super-helpful for. And (2) I don't think that CRUD apps are easy. Well, doubtless some are, but as you say they commonly have huge amounts of complication in them, of a sort that isn't amenable to the kind of formalized reasoning I was talking about.

To answer the implied question in your first sentence: I wasn't trying to make a point, I was giving an answer to a question you asked, namely why mathematical induction might be important for programmers.

Briefer and more explicit version of that answer: For people writing certain kinds of code, understanding mathematical induction makes it easier to reason about that code via techniques such as loop invariants, which makes it easier to make that code bullet-proof. There are many other kinds of code for which nothing closely related to mathematical induction is of any value at all.

(And, to reiterate lest I set the bee in your bonnet buzzing again: Whether a kind of code benefits from this sort of technique has basically nothing to do with how important it is, or how difficult it is to write overall, or what anyone should think of the people writing it.)

It's helpful for truly understanding recursion.

eh, I posit that you already understand induction and just don't know that you do.

"So many CS educated juniors" being uncomfortable with recursion is not an argument against understanding mathematical induction. Who says they understood induction?

You can get a CS degree without understanding induction, and you can understand induction without a CS degree.

I don't know which languages you and your CS educated juniors ("juniors") use.

While "juniors" = employees subordinate to you & "so many "juniors"" = high turnover & you = positive senior employee & college educated graduates = smart: "posit that most CS students don't truly understand recusion" = False '''Smart, being distinct from intelligent, indicates a propensity to make decisions that maximize benefit for the person described as smart. A smart CS student would work for a company that valued intellectual capital instead of a company with high turnover.'''

While "juniors" = employees subordinate to you & "so many "juniors"" = hyperbole & you = positive senior employee: "posit that most CS students don't truly understand recusion" = False '''It is dubious that more than 171.5k CS graduates worked subordinate to you from 2004-2010, or that an unbiased sample of CS graduates from 2004-2010 worked subordinate to you (see previous While "loop") [1] .'''

The proof that the previous comment's posit is not provable follows by induction.

Note_0: While loops can use "&" or "and" operators in some languages without nested loops (unless the programmer chooses to implement a break line) to achieve much of the effect of recursive functions. While statements, as implemented in the example above, offer nearly as much access to the input stack as recursive functions; about equal risk of an infinite loop; and don't risk stack overflow.

Note_1: I have a bachelors in Math. So, I was likely taught a more substantial "theoretical basis," and less "practical skill" than the curriculum most CS graduates were taught.

[1]: http://www.geekwire.com/2014/analysis-examining-computer-sci...

10 I don't see what you added to the discussion

20 But I have to ask, if you have a bachelors in Maths, why do you not know about sample sizes? Or about the flaws in assuming perfect knowledge of actors in a system?

(on reply, GOTO 10)

They are the basis of recursive algorithms proofs, sure you may not need them for everyday programming but that's different for computer science

You need it for a follow-on course, Theory of Computation.