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

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.

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

Replies are listed 'Best First'.
Re^4: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by davido (Cardinal) on Sep 25, 2011 at 05:37 UTC
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	[reply]
Re^5: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by BrowserUk (Patriarch) on Sep 25, 2011 at 06:56 UTC
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'." Thanks for that quote. I'd never heard of that article of Knuth's. I've just skimmed it but will be going back later to read it properly. I have always been a "computer science" sceptic, as I've expounded on at length here several times over the past years: Re: How do you view programming, Re: (OT) Programming as a craft, Re: Programming is more like:. My experience is that each new generation of CS majors come out of college, their heads filled -- by life-long, theoretical computer scientists (aka. professors) -- with idealistic notions of how to use science to produce perfect programs. Then they encounter the real world where they are expected to complete tasks easily as complex as their year long college projects --- using messy real-world data on messy real-world systems with messy real-world languages and tool-sets -- in a few weeks. And for the most part, they forget all the nice theories and knuckle down to doing the job. Those that don't either go back into academia, or write blogs. 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.	[reply]
Re^6: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by davido (Cardinal) on Sep 25, 2011 at 07:26 UTC
Nice link! I may actually have mis-attributed it. Though I thought it was Knuth (and maybe it was), in this article: Structured Programming with Go Go Statements. But since it's a pdf representation of a scan, I can't easily search for the quote therein. Dijkstra did also use it here: On a Cultural Gap. I'm going to have to re-read that Knuth article though; I was almost certain that's where I saw it first. Dave	[reply]
Re^6: 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 25, 2011 at 10:04 UTC
Don't make the assumption that computer science is about programming or computers. To quote Dijkstra: “Computer science is no more about computers than astronomy is about telescopes.”	[reply]
Re^7: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by BrowserUk (Patriarch) on Sep 25, 2011 at 10:47 UTC
Re^4: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by ikegami (Patriarch) on Sep 25, 2011 at 08:50 UTC
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. :(	[reply]
Re^5: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by BrowserUk (Patriarch) on Sep 26, 2011 at 04:05 UTC
Cache misses is another big factor that's usually ignored in theory. Hm. Actually, I think caching has to be ignored. There is simply no way to account for it. On single core processors (without hyper-threading), with single-level caching and fixed processor clock speeds, you can measure the differences between cache-friendly & cache-hostile algorithms -- under very controlled conditions; say single-tasking OS or otherwise quiescent systems -- but you cannot predict them much less formalise them. But once you have multiple, multi-threading cores; with 2 or 3 levels of caching, some per-core, others shared, some split between instructions and data others mixed; dynamically varying clock speeds; variably-timed instructions (think FPU & GPU interactions), out-of-order execution and pipelining; multi-tasking OSs with dynamic priorities and a dynamic mix of hardware and software interrupts; there is simply no way to formalise algorithms to account for any of those sources of non-determinability. Much less all of them. And it is getting harder. Given the rise of virtualisation throwing more and more independent workloads onto each box. Add to that the rise of clustering further increasing the probabilities of cache misses and the benefits of increasing cache sizes starts to fall off very rapidly indeed. Even just measuring performance -- when an operating printer or cooling fan on the same desk can cause enough jiggle on an otherwise static optical mouse, to cause the OS to give a foreground application a priority boost -- is an exercise in futility. Whilst it is possible to demonstrate that under ideal conditions, an algorithm like Judy arrays can -- at a cost of huge complexity -- derive some level of advantage from data locality, relying upon it when so many other random events can sweep the cache out from under you is naive. Personally, I think that the days of trading complexity to achieve speed are long over, at which point the fundamentals of efficient algorithms comes back to exactly the kind of count-the-opcodes instrumentation that Knuth has exemplified for all these years. 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.	[reply]
Re^5: 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:20 UTC
I had a fascinating conversation with Bob Frankston once where he said "Everyone knows that Knuth is wrong in practice" for much the same reason. Improve your skills with Modern Perl: the free book.	[reply]
Re^6: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by ikegami (Patriarch) on Sep 26, 2011 at 06:02 UTC
That reminds me of the link I wanted: You're Doing It Wrong It's not cache misses, it's memory page misses.	[reply]
Re^4: 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 25, 2011 at 09:57 UTC
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.	[reply]
Re^5: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by BrowserUk (Patriarch) on Sep 25, 2011 at 10:43 UTC
Don't forget, open source code is as often not formally proven as commercial code! Sorry. I cannot parse that sentence? Do you mean: open source code is as often as not formally proven as commercial code!? Or maybe: open source code is often not as formally proven as commercial code!? Actually, neither makes sense to me. Nobody formally proves software outside of academia. Even then, that small subset that are formally proven tend to be tiny snippets implementing convenient algorithms on idealised systems, with no time pressures, which if costed at commercial rates would be ruinously expensive. In reality, it doesn't matter, because when I use the phrase "commercial code" I mean code that is written to be used commercially, as opposed to code that is written for academic purposes; and that includes open source software. The nearest equivalents in the motor industry are those design prototypes that they show at events like the Geneva Motor Show, that never get into production. If one car in 50,000 displays a warning light when it shouldn't, the manufacturer recalls millions of them. Just in case. Great example, but wrong argument! I whole heartedly agree that the state of the software industry hasn't yet reached the maturity of the car industry when they were building Model T Fords; and I lamented the typical software disclaimers and what they say about this industry in Re^5: Programming is more like: Car designs aren't proven mathematically. They are tested. Often to destruction. As an example of the futility of trying to use maths as the ultimate design tool for cars, in late 2009 Virgin Racing set out in to design an F1 racing car using only Computational Fluid Dynamics. After two years and close to £100 million during which they rarely came anywhere but last, they recently announced that they were abandoning that policy and are going to rent expertise and facilities -- particularly wind tunnel time -- from one of their competitors. And cars, even F1 cars, probably have less "moving parts" than the (fairly modest) editor I use, and certainly far less complexity than the browser you are viewing this in. 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.	[reply]