Beefy Boxes and Bandwidth Generously Provided by pair Networks
Just another Perl shrine
 
PerlMonks  

Re: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)

by JavaFan (Canon)
on Sep 24, 2011 at 23:05 UTC ( #927692=note: print w/ replies, xml ) Need Help??


in reply to An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)

While on the subject of "limited semantic gotos", I suppose that a purist would consider the use of 'last', 'next', multiple 'return' statements, and in other languages, 'break' to be a form of goto; particularly if a label used.
Uhm, not just a purist. "Goto" is like pregnancy - there isn't a halfway of doing it. Dijkstra's paper isn't about the four letters "g", "o", "t", and "o". His arguments against "goto" hold against "last", "next" and "return" in exactly the same way. Dijkstra's point is, (and IIRC, that's what Dominus wrote as well) that if you want to do any kind of formal proving of your program, life becomes much, much easier if your blocks of code have exactly one entry point, and exactly one exit point. Goto breaks that. And so do "last", "next", "redo", "die", and "return".


Comment on Re: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)
Re^2: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)
by davido (Archbishop) on Sep 25, 2011 at 01:37 UTC

    That is exactly right; an excellent interpretation of Dijkstra's paper and Dominus's analysis! Any block that has more than one entry (this doesn't happen quite as often), or more than one exit (this happens a lot) will be difficult to come up with a formal proof. And this is why last, next, etc., can be seen as "limited semantic" forms of goto.

    As I think it over, I can't come up with any good explanation of where we might jump into code blocks at multiple entry points. An exception might be a given/when block. If fall-through is used, then the block has multiple entry points. And if fall-through isn't used, it has multiple entry and exit points. But on the other hand, given/when can be compared to a chain of if-else blocks, so in that sense perhaps the notion of multiple entry/exit points may sort of break down.

    So where do we have an example of common coding practices that involve multiple entry points?


    Dave

      So where do we have an example of common coding practices that involve multiple entry points?

      Around the time of Dijkstra's paper, computed gotos were both possible and quite common in several prominent languages--Fortran, COBOL, BASIC (not forgetting assembler of all flavours). Later, C's switch, which may superficially resemble an if/elseif/else cascade, is actually a computed goto and far more efficient, as only one condition is ever tested.

      For many purposes, the computed goto -- in the form of C switch statement -- is still invaluable. Almost every generated parser consists of a nest of switch statements.

      Any block that has more than one entry ... or more exit ... will be difficult to come up with a formal proof.

      As a reason (for anything), this is (IMO) a crock. How much commercial code is ever formally proven? Effectively none.

      Why?

      • Because in order to make code provable, it has to be ham-strung in so many ways, that it creates verbosity.
      • Writing code that is provably correct is an order of magnitude harder than writing code that isn't.
      • Once written, you have to pay again to have it proven correct.
      • Verifying that proof is harder than producing it.
      • As is famously claimed, even once you've proven it correct, it doesn't mean it will work.
      • And every time you change anything, you've have to start the proofing again.

      There have been many attempts at producing computer languages that can be formally proven. Very few have ever heard of them and no one uses them. For very good reasons.

      Guard statements, in the form of conditional early returns, nexts & lasts may be hard for the formalists to handle and reason about, but for practical programming, they can and do greatly simplify the handling of exceptional and boundary conditions.

      Formalists don't like handling exceptions. Often this is because they don't have the formal notations for doing do. And when they do invent such notations, they are so complex and shrouded in mystery -- think Haskell's Maybe Monad -- that most people don't understand them.

      Heck. Formalists don't even like handling such practical matters as integer size limitations and floating point inaccuracies. It is often possible to prove an algorithm correct mathematically, only for it to fail horribly and mysteriously when intermediate results are bigger than platform limits for integers or FP values. The classic example is the typical calculation of the mid point in many divide & conquer algorithms. Where mid = ( lo + hi ) / 2 can go out of bounds.

      Ham-stringing the programmer to make life easier for the formal proofing that will never happen is simply bad reasoning.


      Examine what is said, not who speaks -- Silence betokens consent -- Love the truth but pardon error.
      "Science is about questioning the status quo. Questioning authority".
      In the absence of evidence, opinion is indistinguishable from prejudice.

        That's a very thoughtful response, and I appreciate it. Thanks.

        I agree with you that formal proofs never happen in a practical world, and I'm not about to give up 'last', 'next', and multiple return points from subs; they really do seem to make life easier. And often the alternative is additional flags and tests that make the code, as you pointed out, more verbose. They also can make the code more complicated to read, in my opinion.

        While I understand where people are coming from with respect to desiring pure code that can be formally proven, there are precious few people who could even begin to formally prove the algorithm needed to accomplish this "first row" task. I couldn't. But there are those who live in a more theoretical world where producing results in the form of "getting the job done" is a secondary concern.

        Dijkstra may not have been crazy, and MJD's blog does a good job of explaining the reasons. But his sanity existed in the world of computer science rather than the world of computer programming.

        By the way; I liked what Knuth had to say about the term "Computer Science". Paraphrasing, he said, "We wouldn't call surgery 'knife science'." He seemed to consider the term unfortunately applied. ...I don't recall what he thought would have been more applicable though.


        Dave

        Heck. Formalists don't even like handling such practical matters as integer size limitations and floating point inaccuracies.

        Cache misses is another big factor that's usually ignored in theory.

        I can't find the anecdote to which I wanted to link. :(

        How much commercial code is ever formally proven? Effectively none.
        Don't forget, open source code is as often not formally proven as commercial code!

        And it shows. Nowhere except for software do people accept products that are so full of bugs and errors. If one car in 50,000 displays a warning light when it shouldn't, the manufacturer recalls millions of them. Just in case. When it comes to software, people can buy the next version, with a new set of bugs.

      So where do we have an example of common coding practices that involve multiple entry points?
      I wouldn't call it "common", but Duff's Device is an example of multiple entry points.

      In fact, any block of code with labels, and jumps to those labels (or in BASIC, line numbers) has blocks with multiple entry points.

Re^2: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)
by chromatic (Archbishop) on Sep 25, 2011 at 21:23 UTC
    ... if you want to do any kind of formal proving of your program, life becomes much, much easier if your blocks of code have exactly one entry point, and exactly one exit point.

    Certainly a more practical conclusion should be "functional units should do one and only one thing, and that thing well" instead of "avoid obvious flow control at any language level lower than the language primitive which enables functional units". Otherwise you have trouble with if.


    Improve your skills with Modern Perl: the free book.

      Certainly a more practical conclusion should be "functional units should do one and only one thing, and that thing well"
      Eh? I don't follow. How's that even remotely related to having structured blocks?
      avoid obvious flow control at any language level lower than the language primitive which enables functional units". Otherwise you have trouble with if.
      How's that? An if construct is well understood when it comes to formal proofs, and it's a block with exactly one entry, and one exit point:
      ,---> then-block ---, / T \ pre ---> expression ---+ +---> post \ F / `---> else-block ---'

        What's a block, in this context? I'm familiar with basic blocks in terms of SSA and register allocation and flow analysis and optimization. The branch instructions necessary for conditions such as if delimit basic blocks.

        Because you can represent a program in terms of the relationships of these basic blocks, I question the problem of functional analysis. What am I missing?


        Improve your skills with Modern Perl: the free book.

Log In?
Username:
Password:

What's my password?
Create A New User
Node Status?
node history
Node Type: note [id://927692]
help
Chatterbox?
and the web crawler heard nothing...

How do I use this? | Other CB clients
Other Users?
Others imbibing at the Monastery: (7)
As of 2014-12-25 01:36 GMT
Sections?
Information?
Find Nodes?
Leftovers?
    Voting Booth?

    Is guessing a good strategy for surviving in the IT business?





    Results (159 votes), past polls