The Proven Fix

« Return to Article
  • mrtortoise 2009-12-17 09:03
    in first
  • Crash Magnet 2009-12-17 09:09
    mrtortoise:
    in first


    But I'm first, I can prove it!

  • Bosshog 2009-12-17 09:10
    There must be a bug in mathematics!
  • frits 2009-12-17 09:10
    I never thought I'd see the day when a PHD would act arrogantly and be so disconnected from the real world.
  • bored 2009-12-17 09:13
    Agreed, good riddance. I knew something was amiss when they said Dog the Bounty Hunter ;)

    captcha: ingenium != Vijay!
  • RayMarron 2009-12-17 09:14
    Perhaps not coincidently[sic], all of the money-making products were developed and maintained by people without advanced degrees.
    Word.
  • Robert Kosten 2009-12-17 09:16
    "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth, Notes on the van Emde Boas construction of priority deques: An instructive use of recursion
  • dkf 2009-12-17 09:16
    It's hard to make proofs mean jack shit when they hit reality. Speaking as someone who has an advanced degree and does real software engineering. Of course, it's not impossible (I know some people who work in the area of railway signaling systems) but it's expensive and difficult. Only with safety critical work does it really become worth it. For mortals, it's usually better to use the proofs to establish completeness of coverage of the automatic test suite. (Without tests? You're not a software engineer, you're a cowboy code monkey.)
  • Rodnas 2009-12-17 09:20
    Well, it proves that reality has got it wrong again.
  • spxza 2009-12-17 09:23
    I was secretly hoping that the patch would make it into production.

    Damn the man and his stupid simulator.
  • Alargule 2009-12-17 09:27
    Rodnas:
    Well, it proves that reality has got it wrong again.


    I reject reality and substitute my own...arrogance!
  • NotAphD 2009-12-17 09:27
    you lost me when you had the Computer Science phD wearing J Crew.
  • SR 2009-12-17 09:28
    frits:
    I never thought I'd see the day when a PHD would act arrogantly and be so disconnected from the real world.


    [applauds] Frits, you win sarcasm!
  • anon 2009-12-17 09:29
    I used to work with a chap who, when asked to fix a problem, would say that he'd tested each part of the process and proved they were all working fine. That left just one possibility - there was no problem! Except there was...
    Spock was quoted at him regularly.
  • anon 2009-12-17 09:30
    SR:
    frits:
    I never thought I'd see the day when a PHD would act arrogantly and be so disconnected from the real world.


    [applauds] Frits, you win sarcasm!


    And well done ST for spotting it!
  • Kris Leech 2009-12-17 09:31
    This is the best WTF yet! Made me laugh.
  • justsomedude 2009-12-17 09:34
    In theory there is no difference between practice and theory, but in practice there sure as hell is!
  • justsomedude 2009-12-17 09:35
    In theory there is no difference between practice and theory, but in practice there sure as hell is!
  • fourchan 2009-12-17 09:38
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.
  • brazzy 2009-12-17 09:38
    Even when steel prices were highest, 150 tons of steel were worth MUCH less than "millions of dollars" (more like 20,000) - heck, even stuff that might be made from 150 tons of steel and includes a lot of energy and labot costs (e.g. a ship's engine) only has low 6 figure prices AFAIK.
  • aristos_achaion 2009-12-17 09:41
    Evidently, someone has forgotten how easy it is to screw up a proof.
  • dkf 2009-12-17 09:42
    brazzy:
    Even when steel prices were highest, 150 tons of steel were worth MUCH less than "millions of dollars" (more like 20,000) - heck, even stuff that might be made from 150 tons of steel and includes a lot of energy and labot costs (e.g. a ship's engine) only has low 6 figure prices AFAIK.
    If the mix causes (unusual levels of) damage to the mill though, that's when you've got the big costs.
  • SR 2009-12-17 09:45
    brazzy:
    Even when steel prices were highest, 150 tons of steel were worth MUCH less than "millions of dollars" (more like 20,000) - heck, even stuff that might be made from 150 tons of steel and includes a lot of energy and labot costs (e.g. a ship's engine) only has low 6 figure prices AFAIK.


    But if you throw in steel mill equipment* that presumably Vijay was also endangering you'd have that extra zero.

    * yes I know the article didn't specifically say that but let's not split hairs**
    ** yes I know TDWTF's comments section is the last place I should be appealing not to split hairs
  • Dan 2009-12-17 09:47
    He must have trained under one of Dijkstra's disciples. I took a CS course from a professor who was one of Dijkstra's former grad students. It was marked by that famous Dijkstra arrogance, a love of algorithm proofs, and the inability of the professor to code his way out of a wet paper sack.
  • NightDweller 2009-12-17 10:00
    First of all - brillant!
    From now on i am going to remove all my unit tests and replace them with comments detailing the proof of how the system is sure to work correctly!

    Second, what is going on with tdwtf website?
    it was down yesterday and its been malfunctioning today.
    Upgrades? bug fixes? did someone forget the "if it's working don't fix it" rule?
  • bencoder 2009-12-17 10:00
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.


    Heard of Simulated Annealing?
  • hjd 2009-12-17 10:01
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.


    according to The Simpsons, steel mills are full of flamboyant gay guys... This could lead us to the following conclusions:

    * The contributors of TDWTF are working in steel mills
    * The articles on TDWTF are adapted to their readers
    * There is a correlation between hot places and gaping (security) holes
    * The steel industry is more interested in hardware than software

    I'm just going with the flow and changing the subject to pickuplines used by steel industry programmers:

    * You're code looks hawt!
    * I like my permissions strict
    * Is that a stacktrace or are you just glad to see me?
    * Does your party() #include <margaritas.h>?

    I'll stop now...
  • Jack Frots 2009-12-17 10:04
    Robert Kosten:
    "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth, Notes on the van Emde Boas construction of priority deques: An instructive use of recursion

    Well, apparently Knuth is a dunce, because Vijay's work doesn't need trying, only proof.

    captcha: uxor. Latin for "wife". My wife proves over and over that I'm an idiot, but I keep trying...
  • fw 2009-12-17 10:06
    the real WTF is that every line in today's article makes sense.

    ideo campers.
  • vtcodger 2009-12-17 10:12
    ***He must have trained under one of Dijkstra's disciples. I took a CS course from a professor who was one of Dijkstra's former grad students. It was marked by that famous Dijkstra arrogance, a love of algorithm proofs, and the inability of the professor to code his way out of a wet paper sack.***

    Having once been treated to the dubious pleasure of listening to Dijkstra himself droning on and on about some subject far beyond my understanding (and I suspect perhaps his as well), I think I know where you are coming from. "Limited contact area with reality" was my thought at the time.

    However, I have since come to think the "GOTOs Considered Harmful" was about the difficulty/impossibility of understanding/testing software with significant numbers of poorly constrained control transfers. You know ... software like modern GUIs. The stuff that never seems to work quite right. Maybe I didn't give the old guy sufficient credit.

    (Which is not to say that I would ever have released a patch received from anyone based only on a formal proof).
  • Gumpy Gus 2009-12-17 10:20
    So he proved the rest of the program, the compiler, the run-time libraryies, all the device drivers, and the OS were correct?


    Wow, that's quite a guy.


    And, oh, did he prove that his proof was correct? And did he prove that his proof check was correct? ....


  • monkeyPushButton 2009-12-17 10:21
    SR:
    brazzy:
    Even when steel prices were highest, 150 tons of steel were worth MUCH less than "millions of dollars" (more like 20,000) - heck, even stuff that might be made from 150 tons of steel and includes a lot of energy and labot costs (e.g. a ship's engine) only has low 6 figure prices AFAIK.
    But if you throw in steel mill equipment* that presumably Vijay was also endangering you'd have that extra zero.

    * yes I know the article didn't specifically say that but let's not split hairs**
    ** yes I know TDWTF's comments section is the last place I should be appealing not to split hairs
    Don't know much about steel mills, but with molten glass, problems with temperature can cause a loss of more than just the material at the wrong temperature. Having to jackhammer out a tank of solidified (but still several hundred degree) glass is long, hot work that keeps the plant down but everyone busy (and getting paid overtime).
  • Ken B 2009-12-17 10:21
    NightDweller:
    Second, what is going on with tdwtf website?
    it was down yesterday and its been malfunctioning today.
    Upgrades? bug fixes? did someone forget the "if it's working don't fix it" rule?
    But it is working! For the proof, go to prooftp://thedailyftf.com/itsworking.nyah
  • Brandon 2009-12-17 10:21
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.


    Probably the same place that has their furnaces shut down because thousands of tons of coal end up on Pier 53.
  • WhiskeyJack 2009-12-17 10:25
    Actually, I get pretty annoyed too when I've proven that my fix works, and then it doesn't.

    Not so much that I'd leave, though. Otherwise I'd have only been on the job for about a week.
  • Steve H 2009-12-17 10:27
    fw:
    the real WTF is that every line in today's article makes sense.


    Not if you live outside the US. Coffee club? J Crew? Dog the what?
  • SenTree 2009-12-17 10:33
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.
    We recently had a contractor with some steel industry experience. One of his milder anecdotes involved the plant control automation sharing the same network as the office IT. Others included fatalities of the 'flesh and molten steel' don't mix variety (that batch had a higher carbon content than usual...).
  • Ken B 2009-12-17 10:35
    monkeyPushButton:
    Don't know much about steel mills, but with molten glass, problems with temperature can cause a loss of more than just the material at the wrong temperature. Having to jackhammer out a tank of solidified (but still several hundred degree) glass is long, hot work that keeps the plant down but everyone busy (and getting paid overtime).
    I know someone whose family runs a plastic bag manufacturing plant. (All sorts of widths, lengths, thicknesses, etc.) They get raw materials in by the trainload. (Literally. They hook up the car to some hoses, which feed directly into the production process.)

    If something goes wrong, and they need to stop the production line, they lose everything that was already being processed, and they need to re-prime everything once things start up again. I was told that a problem on one production line would cost $10,000 in lost materials alone.

    Okay, so plastics manufacturing and steel mills aren't the same thing. The point is there is often more lost than the one "oopsie".
  • grammer nasty 2009-12-17 10:37
    TRWTF is that American, which often seems logically to simplify English, uses "proven" so often, when "proved" is perfectly good enough and more logical. "Proven" should be kept as an adjective...
  • Seminymous Coward 2009-12-17 10:39
    It's not a proof until a couple of hard, pipe-hittin' professors got to work on it with a pair of pliers and a blow torch... or pencils, I forget which.

    Seriously, y'all are going to unanimously go with "proofs are stupid?" A real proof is a guarantee of correctness. TRWTF is abuse of the word "proof." Even an idiot can say they have a proof.

    Also, if y'all have that much difficulty getting your theory to match real data accurately, your model is what sucks, not the idea of modeling.
  • Big G 2009-12-17 10:44
    Steve H:
    fw:
    the real WTF is that every line in today's article makes sense.


    Not if you live outside the US. Coffee club? J Crew? Dog the what?



    Good point. The coffee club is an employee who provides (as in buys the coffee and runs the coffee maker) coffee to his/her co-workers at cost (typically $0.25/cup aka a quarter for a cup).

    In case your Google isn't working:
    J Crew: Clothing for yuppies.

    Dog the Bounty Hunter In the US if someone does not appear in court they are typically tracked down by a bounty hunter who works for the bail bondsman who floated a loan to bail someone out of jail while they are awaiting trial. Dog is known for um, interesting clothing/hairstyles. Definitely worth looking up a photo if nothing else.
  • DaveyDaveDave 2009-12-17 10:55
    SenTree:
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.
    We recently had a contractor with some steel industry experience. One of his milder anecdotes involved the plant control automation sharing the same network as the office IT. Others included fatalities of the 'flesh and molten steel' don't mix variety (that batch had a higher carbon content than usual...).


    Heh - I have a network admin friend who was employed at the same (I hope there isn't more than one) steel mill, to replace one of the guys who went to prison for criminal negligence, or some such charge.

    He had an anecdote about how his predecessor had bought a large batch of network cards from a rather questionable source. After some time, when several of them had been used to replace faulty cards at various disparate locations around the network, it was discovered that they all had the same MAC address. Hilarity ensued.
  • Zylon 2009-12-17 11:00
    anon:
    I used to work with a chap who, when asked to fix a problem, would say that he'd tested each part of the process and proved they were all working fine. That left just one possibility - there was no problem! Except there was...
    Spock was quoted at him regularly.

    I'm going to assume the Spock quote you're referring to is "When all logical possibilities have been eliminated, whatever remains - however unlikely - must be the truth.", from The Undiscovered Country. Except, this is a Sherlock Holmes quote, which Spock was himself quoting.

    You fail at culture.
  • RBoy 2009-12-17 11:04
    Crash Magnet:
    mrtortoise:
    in first


    But I'm first, I can prove it!



    Best First Ever!*

    * today
  • Mike 2009-12-17 11:08
    This is why I didn't start my Master's degree until I'd been working for a while. Theory and application are such different beasts and you are better if you understand application better than theory rather than the opposite...
  • iToad 2009-12-17 11:08
    For some people, when their model of reality disagrees with reality, then reality is wrong.
  • hoodaticus 2009-12-17 11:09
    SR:
    frits:
    I never thought I'd see the day when a PHD would act arrogantly and be so disconnected from the real world.


    [applauds] Frits, you win sarcasm!


    Frits always wins sarcasm.
  • hoodaticus 2009-12-17 11:11
    Seminymous Coward:
    TRWTF is abuse of the word "proof." Even an idiot can say they have a proof.


    This.
  • dkf 2009-12-17 11:12
    Seminymous Coward:
    Seriously, y'all are going to unanimously go with "proofs are stupid?" A real proof is a guarantee of correctness. TRWTF is abuse of the word "proof." Even an idiot can say they have a proof.
    Well, you see, to do this you throw some equations together and blend (with coffee to lubricate) until you feel in your gut that it has appropriate proofiness.
  • cdosrun 2009-12-17 11:17
    Big G:

    In case your Google isn't working:
    J Crew: Clothing for yuppies.


    I'm not sure "yuppies" will translate either. :-)

    Yuppies traditionally care more about appearance than function. Clothing for yuppies would, stereotypically, be expensive, poorly made, not last very long, and show the Logo of the designer prominently.

    I don't own any J Crew, nor am I familiar with the name, but that's the typical view of the "Yuppie" from my own culture.
  • SenTree 2009-12-17 11:19
    DaveyDaveDave:
    Heh - I have a network admin friend who was employed at the same (I hope there isn't more than one) steel mill, to replace one of the guys who went to prison for criminal negligence, or some such charge.

    He had an anecdote about how his predecessor had bought a large batch of network cards from a rather questionable source. After some time, when several of them had been used to replace faulty cards at various disparate locations around the network, it was discovered that they all had the same MAC address. Hilarity ensued.

    Nice one - how does a rolling mill respond to a carriage return command ?
  • Bob 2009-12-17 11:21
    Yuppie is here in uk but means young up and coming
    expression kinda died in the 80's though :p
  • Sounds Familiar 2009-12-17 11:26
    dkf:
    For mortals, it's usually better to use the proofs to establish completeness of coverage of the automatic test suite. (Without tests? You're not a software engineer, you're a cowboy code monkey.)

    I don't agree that automated tests establish completeness. Performing automated tests only demonstrates that a library or application performs as the test expects it to. It does not prove it actually works as intended.

    I suggest considering that the tests will typically have been written by the same individual that wrote the buggy software to begin with - or someone less capable (like the person in the team who has nothing more important to do and so got assigned to it).

    For that reason, like proofs, automated testing is useful, but should be held has having minimal value (only slightly above "well, the code doesn't generate any compiler warnings").
  • hoodaticus 2009-12-17 11:30
    By "automated testing ... has ... minimal value" I assume you mean other than the immense value in keeping programmers focused on the task at hand.
  • Applied Mathematician 2009-12-17 11:37

    Do you know the difference between theory and practice?

    In theory, there is none.

    In practice, there is.
  • dkf 2009-12-17 11:38
    Sounds Familiar:
    I don't agree that automated tests establish completeness.
    I take it you meant to say “correctness” there? Completeness doesn't really mean very much for most software; there's always something more that could be done if time/effort was available.

    Tests (when proven – there's that word again – to cover a suitable set of functionality) show correctness. Establishing that the test suite is adequate is really hard. The advantage of them over just looking at the code is that you can automatically perform the tests, rather than having to use lots of manual effort. This Is A Good Thing, especially in practice.
  • Neo31337 2009-12-17 11:43
    dkf:
    (Without tests? You're not a software engineer, you're a cowboy code monkey.)


    Lol. Cowboy Code Monkeys unite!!!!

    The 'anti-backup' league needs you!
    (They lost the production code)...

    Mathematically speaking though, a proof (if valid) *is* proof of something (lol)...
    Even Mr Albert's attempt to predict experimental values of General Relativity mathematically didn't correctly align with experimental values detected... The mathematics behind (yummy tensor analysis) were spot on though. So much so that it's really beautiful how well it works when you get down to it (Gotta love the assumed summation with tensor notation).

    All that being said...
    I'm still trying to figure out how one would write up a mathematical proof for MsgBox usage... ;P
  • forgottenlord 2009-12-17 11:47
    I've never met a Comp Sci PhD (or, for that matter, a 4.0 Comp Sci student) that I thought was a good developer
  • Klaus 2009-12-17 11:56
    Zylon:

    I'm going to assume the Spock quote you're referring to is "When all logical possibilities have been eliminated, whatever remains - however unlikely - must be the truth.", from The Undiscovered Country. Except, this is a Sherlock Holmes quote, which Spock was himself quoting.

    You fail at culture.


    Which again is proven because you´re "assuming" something? Awesome!
  • Plz Send Me The Code 2009-12-17 12:01
    forgottenlord :
    But I know PhD's who hire developers to implement their ideas. Why would they want to bother with grunt work?
  • Plz Send Me The Code 2009-12-17 12:02
    hmmm...apparently I need a phd to use this quoting functionality
  • Daniel 2009-12-17 12:13
    Am I the only one who worries if there is a bug in the simulator? (Yes, I know the simulator has been proved right...)

  • junkpile 2009-12-17 12:30
    Sheesh... I thought for sure the story was going to end with the "Avanced Technologies" group somehow being wiped out by a vat of molten steel. Bummer...
  • Bim Job 2009-12-17 12:38
    Klaus:
    Zylon:

    I'm going to assume the Spock quote you're referring to is "When all logical possibilities have been eliminated, whatever remains - however unlikely - must be the truth.", from The Undiscovered Country. Except, this is a Sherlock Holmes quote, which Spock was himself quoting.

    You fail at culture.


    Back we go to the original quote.

    anon:
    I used to work with a chap who, when asked to fix a problem, would say that he'd tested each part of the process and proved they were all working fine. That left just one possibility - there was no problem! Except there was...
    Spock was quoted at him regularly.


    Klaus:
    Which again is proven because you´re "assuming" something? Awesome!
    One throw-away quote, with no implication of "proof" attached, and you're getting steamed up for some reason?

    Not that I'd claim that Sherlock Holmes is exactly "culture." The original quote is, however, a far better guide-line for anybody working with computers:

    It is an old maxim of mine that when you have excluded the impossible, whatever remains, however improbable, must be the truth. (The Adventure of the Beryl Coronet, fwiw.)

    In this particular case, Sherlock's maxim is far more relevant. Merely running a set of tests, however fine those tests might be, does not "exclude the impossible."
  • Bim Job 2009-12-17 12:47
    Robert Kosten:
    "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth, Notes on the van Emde Boas construction of priority deques: An instructive use of recursion
    Wins for today's most relevant quote.

    A lot of my friends are Vijays, and I've got to say that this is the first time I've come across one who is clearly an abject moron.

    I've got another friend who was charged with writing a "real time compiler" (in his words) to determine what to do with several tons of molten steel at the other end of the rollers. Kicking off a full 45 seconds before the steel hit the back wall.

    A wonderful opportunity for a 22 year old graduate, I feel. I've never been comfortable round steel mills since.
  • MrKltpzyxm 2009-12-17 12:51
    Somebody beat me to it but I'm going to post it anyway. Whenever reality disagrees with me, reality must be wrong.
  • Somebody 2009-12-17 12:59
    Proving the correctness of a system does actually work and is sometimes done with very critical systems.

    But you need to build the system with those formal methods from ground up, you cannot just try to prove stuff about normal systems that have the occational hack here and there.
    If you start making assumptions about how the progam behaves you always get it wrong.
  • halcyon1234 2009-12-17 13:14
    justsomedude:
    In theory there is no difference between practice and theory, but in practice there sure as hell is!


    A consultant is someone who takes what works in practice and tries to put it on paper...
  • pizzaguy 2009-12-17 13:26
    Applied Mathematician:

    Do you know the difference between theory and practice?

    In theory, there is none.

    In practice, there is.


    I did, actually. It was already posted twice.
  • Dave 2009-12-17 13:32
    Oh for deity's sake.

    Spock is most famous for saying 'Illogical'. Which would be a quote that would actually make sense in the context above. I don't see any reason to bring Sherlock Holmes into it. His brother Mycroft the High Optional, Logical, Multi-Evaluating Supervisor is more relevant...

    Now that someone has, though, I have to point out that the 'Having excluded... whatever remains must be the truth' quote is illogical itself. It would be more accurate to say 'whatever remains must include the truth, as well as other untrue possibilities'.

    Incidentally:

    "CAPTCHA Test (Required For Anonymous Users)
    Prove that you're not a robot."

    That test proves nothing of the kind. I may just be a robot with Captcha reading abilities...
  • repoman 2009-12-17 13:36
    Dan:
    He must have trained under one of Dijkstra's disciples. I took a CS course from a professor who was one of Dijkstra's former grad students. It was marked by that famous Dijkstra arrogance, a love of algorithm proofs, and the inability of the professor to code his way out of a wet paper sack.

    If you're in a wet paper sack and want to get out, starting up your favourite IDE isn't the way to go about it.
  • udo the valet 2009-12-17 13:37
    Ken B:
    For the proof, go to prooftp://thedailyftf.com/itsworking.nyah


    There's a proof transfer protocol?
  • cconroy 2009-12-17 13:53
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.

    Wait 'til you read the one about the liquid nitrogen tanker crash. It took *weeks* to clean up that mess.
  • Zork II 2009-12-17 13:59
    Nothing wrong with good old mathematical proof - used it myself and got some very good systems out of it. Problem comes when certain academics forget that in the "real-world" compilers, linkers, operating systems, hardware etc *will* fsck things up.

    Of course trying to tell all this to a formal methods professor who doesn't have hands-on experience is doomed to fail.

    Rarely do people use formal methods correctly anyway...
  • Bim Job 2009-12-17 14:04
    Dave:
    Oh for deity's sake.

    Spock is most famous for saying 'Illogical'. Which would be a quote that would actually make sense in the context above. I don't see any reason to bring Sherlock Holmes into it. His brother Mycroft the High Optional, Logical, Multi-Evaluating Supervisor is more relevant...

    Now that someone has, though, I have to point out that the 'Having excluded... whatever remains must be the truth' quote is illogical itself. It would be more accurate to say 'whatever remains must include the truth, as well as other untrue possibilities'.

    Incidentally:

    "CAPTCHA Test (Required For Anonymous Users)
    Prove that you're not a robot."

    That test proves nothing of the kind. I may just be a robot with Captcha reading abilities...
    It is an old maxim of mine that when you have excluded the impossible, whatever remains, however improbable, must be the truth.

    You are correct. It is not impossible that you are a robot with Captcha reading abilities. You have therefore not excluded the impossible.

    The requirement to "prove that you're not a robot" does not imply that, having passed a weak test of proof, you are not a robot.

    That would be illogical, captain.
  • Tzimisce 2009-12-17 14:04
    Sounds Familiar:
    automated testing is useful, but should be held has having minimal value (only slightly above "well, the code doesn't generate any compiler warnings").


    I strongly disagree. This WTF shows just how valuable integration testing can be. The alternative of placing it into production and seeing if the steel is ruined is less attractive to me.

    It's all about layering tests - isolated unit tests (with continuous integration to run them automatically on every check-in), integration tests, and user acceptance tests (possibly with other types of tests as well). Automating the majority of this insures that the tests are actually run.

    Testing is a skill, and does require training and/or experience. But using TDD, I have found bugs in code that I've written that I would not have caught otherwise until much later in the development process.
  • arty 2009-12-17 14:11
    Seminymous Coward:
    Seriously, y'all are going to unanimously go with "proofs are stupid?" A real proof is a guarantee of correctness. TRWTF is abuse of the word "proof." Even an idiot can say they have a proof.


    Unfortunately, mathematics can't prove much about about complicated programs in unrestricted turing machines.

    Why don't we have standard support for making objects into communicating sequential processes in the standard library of any language? Why don't we have a finite automaton other than regex(3) in the standard library?
  • Bim Job 2009-12-17 14:20
    Somebody:
    Proving the correctness of a system does actually work and is sometimes done with very critical systems.

    But you need to build the system with those formal methods from ground up, you cannot just try to prove stuff about normal systems that have the occational hack here and there.
    If you start making assumptions about how the progam behaves you always get it wrong.
    Not a quote, per se, but today's second best point.

    There's an obvious distinction between systems that need to be built on formal proofs (a very small number, but not negligible), and systems that are engineered: ie, those that have a certain tolerance and can be tested via an increasingly narrowed set of unit and regression tests.

    Then again, there's always PHP.
  • Anon 2009-12-17 14:32
    Seminymous Coward:
    Seriously, y'all are going to unanimously go with "proofs are stupid?" A real proof is a guarantee of correctness. TRWTF is abuse of the word "proof." Even an idiot can say they have a proof.

    Also, if y'all have that much difficulty getting your theory to match real data accurately, your model is what sucks, not the idea of modeling.


    A proof is a guarantee of correctness when all assumptions hold true. It's very rare for those assumptions to cover everything that applies in reality and sometimes it does matter. Infinite precision is, for example, an assumption often used which doesn't hold in real life. Floating point inaccuracies can in fact be larger than the theoretical error bounds in some cases. The assumption that you can pay a guy $20/hr to do something instead of a computer is also usually ignored even if that strategy beats all the theoretical ones.
  • ounos 2009-12-17 14:36
    Dan:
    He must have trained under one of Dijkstra's disciples. I took a CS course from a professor who was one of Dijkstra's former grad students. It was marked by that famous Dijkstra arrogance, a love of algorithm proofs, and the inability of the professor to code his way out of a wet paper sack.

    Arrogance? Dijkstra? The same Dijkstra who wrote "The Humble Programmer"?
  • wingcommander 2009-12-17 15:02
    You attempt to explain cultural strangeness in the US is appreciated. However you have skipped the weird part. The weird part: Dog the Bounty Hunter is a TV show.

    Really.

  • Matt Westwood 2009-12-17 15:13
    No WTF here, just a typical story of a learning experience of a witless genius.

    The reason this does <b>not</b> make a WTF is the insistence on the use of a simulation. I can't praise simulations enough. My first large-scale professional job was the mathematical design for a gunfire control system for on board ship. We designed it around the simulation that we had programmed. Having proved the algorithms on that simulation (after several false starts), documented it carefully in pseudocode, farmed it out to the codewriters and built it into the system, we took it on board the customer's ship, plugged it in and switched it on, and it worked first time perfectly. It was the first ever commercial system ever delivered in Ada, delivered on time and within budget. And all because of our sweet little simulation. Happy days.
  • hoodaticus 2009-12-17 15:16
    The other RWTF is that Vijay didn't break into the simulator at midnight to test his fix in secret before he went bragging about his "proof". Leave it to a PhD to fail at CYA.
  • Zero Sum 2009-12-17 15:26
    "I'm telling you Robert, you're going to really appreciate having Vijay around," said Phil, "He interviewed real strong and, get this. He has a PhD in Computer Science! You'll be thanking me by the end of next week, you'll see!"

    He may have a degree, but Vijay is no Scientist. Real Scientists confirm their hypothesis through experiment, even Computer Scientists.
  • Bim Job 2009-12-17 15:28
    Matt Westwood:
    No WTF here, just a typical story of a learning experience of a witless genius.

    The reason this does <b>not</b> make a WTF is the insistence on the use of a simulation. I can't praise simulations enough. My first large-scale professional job was the mathematical design for a gunfire control system for on board ship. We designed it around the simulation that we had programmed. Having proved the algorithms on that simulation (after several false starts), documented it carefully in pseudocode, farmed it out to the codewriters and built it into the system, we took it on board the customer's ship, plugged it in and switched it on, and it worked first time perfectly. It was the first ever commercial system ever delivered in Ada, delivered on time and within budget. And all because of our sweet little simulation. Happy days.
    Or just dumb blind luck.
  • iToad 2009-12-17 15:30
    hoodaticus:
    The other RWTF is that Vijay didn't break into the simulator at midnight to test his fix in secret before he went bragging about his "proof". Leave it to a PhD to fail at CYA.


    It's the difference between being smart and being street smart.
  • Matt Westwood 2009-12-17 15:39
    Bim Job:
    Matt Westwood:
    No WTF here, just a typical story of a learning experience of a witless genius.

    The reason this does <b>not</b> make a WTF is the insistence on the use of a simulation. I can't praise simulations enough. My first large-scale professional job was the mathematical design for a gunfire control system for on board ship. We designed it around the simulation that we had programmed. Having proved the algorithms on that simulation (after several false starts), documented it carefully in pseudocode, farmed it out to the codewriters and built it into the system, we took it on board the customer's ship, plugged it in and switched it on, and it worked first time perfectly. It was the first ever commercial system ever delivered in Ada, delivered on time and within budget. And all because of our sweet little simulation. Happy days.
    Or just dumb blind luck.


    No, not luck, although we might have thought so at the time. But then we repeated the design process, er, repeatedly. With the same level of success.
  • Bim Job 2009-12-17 15:46
    Matt Westwood:
    Bim Job:
    Matt Westwood:
    No WTF here, just a typical story of a learning experience of a witless genius.

    The reason this does <b>not</b> make a WTF is the insistence on the use of a simulation. I can't praise simulations enough. My first large-scale professional job was the mathematical design for a gunfire control system for on board ship. We designed it around the simulation that we had programmed. Having proved the algorithms on that simulation (after several false starts), documented it carefully in pseudocode, farmed it out to the codewriters and built it into the system, we took it on board the customer's ship, plugged it in and switched it on, and it worked first time perfectly. It was the first ever commercial system ever delivered in Ada, delivered on time and within budget. And all because of our sweet little simulation. Happy days.
    Or just dumb blind luck.


    No, not luck, although we might have thought so at the time. But then we repeated the design process, er, repeatedly. With the same level of success.
    <citation needed>
  • SBev 2009-12-17 16:17
    Lol.. try having a Astro Physicist PhD as a developer. Shot for the stars, but missed.
  • BdH 2009-12-17 16:24
    Like many others, I work in embedded controllers. I'm in the software team, and of course there is a corresponding hardware team.

    As can be expected, there are those in the software team who blame all problems reflexively on bad hardware, and an equal number of hardware team members who instinctively blame the software for all ills.

    While this goes by, the more jaded members of the teams work together to actually fix the problem of the day. We've all seen cases where it absolutely could not be our soft/hardware, it must be their hard/software, but at the end of the day, it really was us. So usually, we leave our egos at the door, try to work together and find the problem and/or some third party to blame (vendor, requirements, interface spec, etc.).

    Generally speaking, things work out.

    In years gone by, the old (read: ancient) head of The Hardware Team retired, and a Vijay type came in to replace him. At this point, the "hardware is fine, it's your software" rhetoric meter immediately went to 11, and stayed there.

    The I/O test failed? Software.

    New system board was literally emitting smoke when powered up? Software.

    Screen is dark? Software (hint: software works better with the power on).

    It didn't matter what the question was, the answer was "it's software's fault".

    One day, a customer came in to run a V&V on some units before signing off. These units being six figure items, it's not surprising that this is a contractual requirement.

    Two units passed the burn-in and 8 hour validation by V&V, with the customer witnessing and/or participating every step of the way.

    On the third day, the third unit failed during power up. Vijay stormed into the software team area, absolutely livid.

    "Your software", he started, "just failed! In front of the customer! We could lose a major sale! You have to fix it. Now!". Vijay was beside himself at this point.

    "Okay, so how did the software fail?", I ask. While there was always a chance that something really was wrong in the code, the fact that two units had already passed the V&V tests filled me with a certain level of confidence.

    "It says there was a hardware fault, and the customer won't accept it like that!", Vijay practically spit. "You have to change the software to say that the hardware's working!".

    Sighs all around in the software room, as coders returned to their workstations/mountain dew/crossword puzzles/dilbert of the day, etc.

    "Well Vijay", I asked, "have you ever considered the possibility that the software might actually have found a problem in the hardware? I mean, this is the HARDWARE SELF TEST software you're running, right?"

    Numerous claims that there are no problems with the hardware, after all, two units already passed, etc.

    At this point senior management (to a VP level) starts streaming in, trying to turn an on-site unhappy customer into a happy one. The customer rep himself is there. This has now ceased being a technical discussion and become a political one.

    The VP of tech (my boss, and Vijay's) decrees that we'll pop open the box in question, and look at the board that the software claims is bad. We do so, and swap the bad board with another board type from a unit that's already passed internal V&V.

    We rerun the preliminary tests. Lo and behold, the failing unit (now with a good board) passes. And the previously working unit (now with the swapped board) fails the power on self-test. Go figure. The customer nods; we'll restart the tests with this unit, and use it for unit 3.

    At this point, the VP looks at Vijay, and says "well, I'd say that pretty much confirms whether it's software or hardware, wouldn't you say?"

    "Of course!", Vijay said, close to yelling. "Their software is so bad it's not even predictable! This is why it takes so long to build good hardware! The test software is unreliable!".

    The software people sighed.

    The hardware people grimaced and/or quietly left the room.

    The customer's eyes got really big.

    The VP resembled a small, furry animal, trapped in the headlights of an oncoming car.

    This was later described as a "jaw/floor" moment.

    The unit was tested, the customer was happy (far more so than our VP), and it was shortly announced that our Vijay was to be "side-moted" to the Mechanical division. Vijay complained he wouldn't be able to do much in his new position, to which the VP replied, "that's pretty much the point".

    Occasionally, executives do get it right.

  • Matt Westwood 2009-12-17 16:24
    Bim Job:
    Matt Westwood:
    Bim Job:
    Matt Westwood:
    No WTF here, just a typical story of a learning experience of a witless genius.

    The reason this does <b>not</b> make a WTF is the insistence on the use of a simulation. I can't praise simulations enough. My first large-scale professional job was the mathematical design for a gunfire control system for on board ship. We designed it around the simulation that we had programmed. Having proved the algorithms on that simulation (after several false starts), documented it carefully in pseudocode, farmed it out to the codewriters and built it into the system, we took it on board the customer's ship, plugged it in and switched it on, and it worked first time perfectly. It was the first ever commercial system ever delivered in Ada, delivered on time and within budget. And all because of our sweet little simulation. Happy days.
    Or just dumb blind luck.


    No, not luck, although we might have thought so at the time. But then we repeated the design process, er, repeatedly. With the same level of success.
    <citation needed>


    http://books.google.co.uk/books?id=l-DzknmTgDUC&pg=PA116&lpg=PA116&dq=gp250+ferranti&source=bl&ots=2rgKA0phKl&sig=7O-BwJ5uz5g31JqX0Z1tkOrFVzo&hl=en&ei=OaEqS-mlDcj84AaaqNmOCQ&sa=X&oi=book_result&ct=result&resnum=1&ved=0CAoQ6AEwAA#v=onepage&q=gp250%20ferranti&f=false
  • Seminymous Coward 2009-12-17 16:48
    arty:
    Unfortunately, mathematics can't prove much about about complicated programs in unrestricted turing machines.


    It works well for a specific, known program. It works poorly for an arbitrary, variable program. By that, I mean that a particular program on a particular system is a much easier target for a proof than the space of all programs. This applies especially if the particular program is written with formal methods in mind.

    Anon:
    A proof is a guarantee of correctness when all assumptions hold true. It's very rare for those assumptions to cover everything that applies in reality and sometimes it does matter. Infinite precision is, for example, an assumption often used which doesn't hold in real life. Floating point inaccuracies can in fact be larger than the theoretical error bounds in some cases.


    People good at numerical analysis know this and track the inaccuracies to get correct error bounds. The naive model of infinite accuracy is a bad model for a floating-point unit. Numerical analysts therefore use a more accurate model; if you want to think about it, a still somewhat weak choice is to model floating-point units as acting on intervals of the real line.
  • campkev 2009-12-17 16:58
    repoman:
    Dan:
    He must have trained under one of Dijkstra's disciples. I took a CS course from a professor who was one of Dijkstra's former grad students. It was marked by that famous Dijkstra arrogance, a love of algorithm proofs, and the inability of the professor to code his way out of a wet paper sack.

    If you're in a wet paper sack and want to get out, starting up your favourite IDE isn't the way to go about it.


    You've obviously never used MY favorite IDE.
  • Maurits 2009-12-17 17:31
    Story fail.

    What was wrong with the patch?

    What was wrong with the proof?
  • F 2009-12-17 17:56
    I'm not sure that code would be my tool of choice for getting out of one of those. Then again, I've never tried it, so ...
  • DC 2009-12-17 18:04
    Bim Job:
    Robert Kosten:
    "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth, Notes on the van Emde Boas construction of priority deques: An instructive use of recursion
    Wins for today's most relevant quote.

    A lot of my friends are Vijays, and I've got to say that this is the first time I've come across one who is clearly an abject moron.

    I've got another friend who was charged with writing a "real time compiler" (in his words) to determine what to do with several tons of molten steel at the other end of the rollers. Kicking off a full 45 seconds before the steel hit the back wall.

    A wonderful opportunity for a 22 year old graduate, I feel. I've never been comfortable round steel mills since.


    Final acceptance test: Stand between roller and back wall.

    Either way, a problem is solved.
  • MadX 2009-12-17 18:22
    Vijay sounds like my sister before the sex change operation.
  • anon 2009-12-17 18:36
    I don't get it - nobody has mentioned that perhaps the simulator itself has the bug?

    Perhaps the code correctly sets the temperature to 256 degrees (or whatever), but due to sign issues in the simulator it displays it as -255... Thus the code is ok, but the simulator is buggy.
  • katastrofa 2009-12-17 18:43
    Gumpy Gus:
    So he proved the rest of the program, the compiler, the run-time libraryies, all the device drivers, and the OS were correct?


    Wow, that's quite a guy.


    And, oh, did he prove that his proof was correct? And did he prove that his proof check was correct? ....




    How do you test that the tests are correct?

    How do you prove that your perception of reality ("tests don't work", "code does not compile") is correct?

    How do you prove you're not just a brain in a jar talking to electrodes?
  • suscipere 2009-12-17 19:03
    NightDweller:
    First of all - brillant!
    From now on i am going to remove all my unit tests and replace them with comments detailing the proof of how the system is sure to work correctly!

    Second, what is going on with tdwtf website?
    it was down yesterday and its been malfunctioning today.
    Upgrades? bug fixes? did someone forget the "if it's working don't fix it" rule?
    Naw, it's just been Bowytzed.

    Hope you read this comment soon, before Mark get's his panties back inna twist.
  • abigo 2009-12-17 19:06
    Steve H:
    fw:
    the real WTF is that every line in today's article makes sense.


    Not if you live outside the US. Coffee club? J Crew? Dog the what?
    <3 u.
  • me 2009-12-17 19:24
    Big G:


    Dog the Bounty Hunter...Definitely worth looking up a photo if nothing else.


    It's worth looking up 'Vijay' in Google images as well. I can picture the guy now.
  • Ouch! 2009-12-17 19:28
    BdH:
    to which the VP replied, "that's pretty much the point".

    Wow, how did such a lucid person ever get promoted to VP?
    Anyway, do your best to keep him around as long as possible.
  • Jase 2009-12-17 19:39
    cdosrun:
    Big G:

    In case your Google isn't working:
    J Crew: Clothing for yuppies.


    I'm not sure "yuppies" will translate either. :-)

    Yuppies traditionally care more about appearance than function. Clothing for yuppies would, stereotypically, be expensive, poorly made, not last very long, and show the Logo of the designer prominently.

    I don't own any J Crew, nor am I familiar with the name, but that's the typical view of the "Yuppie" from my own culture.


    It's a bastardisation of an acronym (I can't exactly remember what for, but it's something like Young Upwardly-mobile Professional)

    Basically it refers to people who have more dollars than sense and like to show off what they consider to be their immense wealth
  • Blinkin 2009-12-17 19:44
    Sounds Familiar:
    dkf:
    For mortals, it's usually better to use the proofs to establish completeness of coverage of the automatic test suite. (Without tests? You're not a software engineer, you're a cowboy code monkey.)

    I don't agree that automated tests establish completeness. Performing automated tests only demonstrates that a library or application performs as the test expects it to. It does not prove it actually works as intended.

    I suggest considering that the tests will typically have been written by the same individual that wrote the buggy software to begin with - or someone less capable (like the person in the team who has nothing more important to do and so got assigned to it).

    For that reason, like proofs, automated testing is useful, but should be held has having minimal value (only slightly above "well, the code doesn't generate any compiler warnings").


    What a peculiar thing to say, sounds to me like:
    a) The test shouldn't be written by anyone who understands how the program works 'under the hood'
    b) The testing shouldn't be done by anyone who doesn't understand the intricacies of the program
    They sound a little opposing to me....


    That said, I'm a big fan of seperate teams of testers, who understand an application, but not necessarily how those applications work. They can then test expected functionality, with no bias for or against corner cases (other than obvious ones like value=0).
    I think the original author of the code has some responsibility to do fairly basic testing, however I would imagine for most programmers personal pride means that they've tested it enough to be absolutely certain that it works (and then get upset when the testers identify that it doesn't)
  • Blinkin 2009-12-17 19:46
    Sounds Familiar:
    dkf:
    For mortals, it's usually better to use the proofs to establish completeness of coverage of the automatic test suite. (Without tests? You're not a software engineer, you're a cowboy code monkey.)

    I don't agree that automated tests establish completeness. Performing automated tests only demonstrates that a library or application performs as the test expects it to. It does not prove it actually works as intended.

    I suggest considering that the tests will typically have been written by the same individual that wrote the buggy software to begin with - or someone less capable (like the person in the team who has nothing more important to do and so got assigned to it).

    For that reason, like proofs, automated testing is useful, but should be held has having minimal value (only slightly above "well, the code doesn't generate any compiler warnings").


    Oh, and I missed a bit of your point (sorry)

    I think Automated testing can (when used properly, and made by competent testers) be a very valuable regression testing and/or load testing tool.
  • Shinobu 2009-12-17 20:14
    A proof is essentially a construct that turns assumptions into a conclusion using reasoning steps. If the conclusion is proven wrong by reality, that means one of two things:
    1) A reasoning step was wrong. I don't know how many proofs (including my own) I've sent back to the drawing board by asking the why question. Or sometimes simply: ‘Wait a minute...’ People make reasoning errors.
    2) One of the assumptions was wrong.
    And this is why I think they should have studied the proof longer. They agreed to the proof, so I assume they checked the reasoning thoroughly, which means that one of the assumptions behind the proof about how the system operates is false. In other words, the real system isn't behaving like the system in their minds.
    Now, of course I can't tell from my comfy chair what's wrong. Some people say the simulator may be buggy, but I doubt that is causing the problem. After all, it displays the same faulty reading as the real system in the same conditions.
    All I can say is that there is potentially a lot to be gained from studying faulty proofs. For example, an acquaintance of a friend of mine studies clinical trials of homoeopathy and that can teach us a lot about faults in trials and human reasoning about statistics. So don't trash proofs. They are a bit like unit tests of the human mind and you disregard them at your peril.
  • Mike 2009-12-17 20:40
    I'm curious, is it possible to prove things like finishing within a certain execution time or working within the numerical limits of the hardware?
  • db 2009-12-17 20:48
    fourchan:
    I think this is the third steel mill article. I wonder if it's a product of anonymization or if steel mills are actually such WTFy places.


    Every steel mill I've been to has holes in the roof from some major WTF incident. That even includes one rod rolling mini-mill that was less than six months old with a roof height as high as about a third of the length of the entire rolling line.
  • hoodaticus 2009-12-17 20:59
    Mike:
    I'm curious, is it possible to prove things like finishing within a certain execution time or working within the numerical limits of the hardware?


    Is assembly language on given equipment, sure.

    Addendum (2009-12-17 21:05):
    I mean "in", not "is".
  • Watson 2009-12-17 21:15
    Shinobu:
    Now, of course I can't tell from my comfy chair what's wrong. Some people say the simulator may be buggy, but I doubt that is causing the problem. After all, it displays the same faulty reading as the real system in the same conditions.
    We don't actually know this either; it may be (I hope it is) the case that the bug was detected no later than during simulation and hadn't yet escaped into the real world.

    It is of course also possible that it was first spotted in the wild and only picked up during simulation when the latter was put through the specific scenario that triggered it - we don't know how comprehensively the simulation was put through its paces - but that would make for two bugs: the real-world one and the lacuna in the testing regime.
  • Watson 2009-12-17 21:16
    Mike:
    I'm curious, is it possible to prove things like finishing within a certain execution time or working within the numerical limits of the hardware?
    The first one is easy enough: run the program (you are talking about a program, right?) for the requisite length of time and see if it finishes.
  • lolwtf 2009-12-17 22:02
    Gumpy Gus:
    So he proved the rest of the program, the compiler, the run-time libraryies, all the device drivers, and the OS were correct?


    Wow, that's quite a guy.


    And, oh, did he prove that his proof was correct? And did he prove that his proof check was correct? ....
    Yep. Turned out to be a hardware problem.


    Actually, I'd be very amused if it were that, or user error, or his patch never actually got applied, etc.
  • A Gould 2009-12-17 22:12
    Maurits:
    Story fail.

    What was wrong with the patch?

    What was wrong with the proof?


    - The problem with the patch is that it didn't fix the problem.

    - The problem with the proof is probably related to the fact that he "solved" their software the same afternoon that he started with the company. (He was shown around the office in the morning, given a bug-fix, and brought his proof in the afternoon). That's not really enough time to develop a formal proof of a piece of software.
  • arty 2009-12-17 22:27
    hoodaticus:
    Mike:
    I'm curious, is it possible to prove things like finishing within a certain execution time or working within the numerical limits of the hardware?


    In assembly language on given equipment, sure.

    Addendum (2009-12-17 21:05):
    I mean "in", not "is".


    Here is a function of one argument, in assembly. Can you prove that it halts in finite time for any positive input less than 1 billion without trying them all?


    000000000040058c <foo>:
    40058c: 55 push %rbp
    40058d: 48 89 e5 mov %rsp,%rbp
    400590: 48 83 ec 30 sub $0x30,%rsp
    400594: 48 89 7d f8 mov %rdi,-0x8(%rbp)
    400598: 48 89 75 f0 mov %rsi,-0x10(%rbp)
    40059c: 48 83 7d f8 02 cmpq $0x2,-0x8(%rbp)
    4005a1: 74 56 je 4005f9 <foo+0x6d>
    4005a3: 48 8b 45 f0 mov -0x10(%rbp),%rax
    4005a7: 48 83 c0 01 add $0x1,%rax
    4005ab: 48 89 45 e0 mov %rax,-0x20(%rbp)
    4005af: 48 8b 45 f8 mov -0x8(%rbp),%rax
    4005b3: 83 e0 01 and $0x1,%eax
    4005b6: 84 c0 test %al,%al
    4005b8: 74 18 je 4005d2 <foo+0x46>
    4005ba: 48 8b 45 f8 mov -0x8(%rbp),%rax
    4005be: 48 89 c2 mov %rax,%rdx
    4005c1: 48 01 d2 add %rdx,%rdx
    4005c4: 48 8d 04 02 lea (%rdx,%rax,1),%rax
    4005c8: 48 83 c0 01 add $0x1,%rax
    4005cc: 48 89 45 e8 mov %rax,-0x18(%rbp)
    4005d0: eb 15 jmp 4005e7 <foo+0x5b>
    4005d2: 48 8b 55 f8 mov -0x8(%rbp),%rdx
    4005d6: 48 89 d0 mov %rdx,%rax
    4005d9: 48 c1 e8 3f shr $0x3f,%rax
    4005dd: 48 01 d0 add %rdx,%rax
    4005e0: 48 d1 f8 sar %rax
    4005e3: 48 89 45 e8 mov %rax,-0x18(%rbp)
    4005e7: 48 8b 75 e0 mov -0x20(%rbp),%rsi
    4005eb: 48 8b 7d e8 mov -0x18(%rbp),%rdi
    4005ef: e8 98 ff ff ff callq 40058c <foo>
    4005f4: 89 45 dc mov %eax,-0x24(%rbp)
    4005f7: eb 07 jmp 400600 <foo+0x74>
    4005f9: 48 8b 45 f0 mov -0x10(%rbp),%rax
    4005fd: 89 45 dc mov %eax,-0x24(%rbp)
    400600: 8b 45 dc mov -0x24(%rbp),%eax
    400603: c9 leaveq
    400604: c3 retq

  • hol 2009-12-17 23:33
    Didn't I hear this steel mill thing before? I only got past the introductory paragraph, but hey, I grew up on slashdot.
  • SQLDave 2009-12-17 23:56
    Rodnas:
    Well, it proves that reality has got it wrong again.


    Vijay must have been an HGTTG disciple.

    "...though it cannot hope to be useful or informative on all matters, it does make the reassuring claim that where it is inaccurate, it is at least definitively inaccurate. In cases of major discrepancy it was always reality that's got it wrong."

    --Douglas Adams (RIP)
  • Planck 2009-12-18 00:57
      400594:       48 89 7d f8             mov    %rdi,-0x8(%rbp)
    
    400598: 48 89 75 f0 mov %rsi,-0x10(%rbp)


    That's not a function of one argument, it's a function of two arguments.
  • RogerInHawaii 2009-12-18 01:16
    iToad:
    For some people, when their model of reality disagrees with reality, then reality is wrong.


    Such is the way of Republicans.
  • Robert Kosten 2009-12-18 01:43
    Jase:
    cdosrun:
    Big G:

    In case your Google isn't working:
    J Crew: Clothing for yuppies.


    I'm not sure "yuppies" will translate either. :-)

    Yuppies traditionally care more about appearance than function. Clothing for yuppies would, stereotypically, be expensive, poorly made, not last very long, and show the Logo of the designer prominently.

    I don't own any J Crew, nor am I familiar with the name, but that's the typical view of the "Yuppie" from my own culture.


    It's a bastardisation of an acronym (I can't exactly remember what for, but it's something like Young Upwardly-mobile Professional)

    Basically it refers to people who have more dollars than sense and like to show off what they consider to be their immense wealth

    I was under the impression it was "Young urban professional", I've always liked "dinks" (Double income, no kids), too :-)
  • Matt Westwood 2009-12-18 02:52
    Blinkin:
    Sounds Familiar:
    dkf:
    For mortals, it's usually better to use the proofs to establish completeness of coverage of the automatic test suite. (Without tests? You're not a software engineer, you're a cowboy code monkey.)

    I don't agree that automated tests establish completeness. Performing automated tests only demonstrates that a library or application performs as the test expects it to. It does not prove it actually works as intended.

    I suggest considering that the tests will typically have been written by the same individual that wrote the buggy software to begin with - or someone less capable (like the person in the team who has nothing more important to do and so got assigned to it).

    For that reason, like proofs, automated testing is useful, but should be held has having minimal value (only slightly above "well, the code doesn't generate any compiler warnings").


    Oh, and I missed a bit of your point (sorry)

    I think Automated testing can (when used properly, and made by competent testers) be a very valuable regression testing and/or load testing tool.


    All these people who consider that unit testing is of limited use are probably the same ones who have never actually worked on a system with full and comprehensive modular testing strategy. Don't worry, their loss, all the less competition in the universe for quality software.
  • Herby 2009-12-18 03:41
    DaveyDaveDave:


    Heh - I have a network admin friend who was employed at the same (I hope there isn't more than one) steel mill, to replace one of the guys who went to prison for criminal negligence, or some such charge.

    He had an anecdote about how his predecessor had bought a large batch of network cards from a rather questionable source. After some time, when several of them had been used to replace faulty cards at various disparate locations around the network, it was discovered that they all had the same MAC address. Hilarity ensued.


    Ah... Same MAC addresses. I know a bit about this. I knew a company that produced serialized PROMS that had MAC addresses for a network card vendor. They network card vendor contracted out the assembly, and specified that the PROM be single sourced (from my friend). The contract assembly house in an attempt to cheapen the build decided on their own to make the part themselves, and having a "sample" they just peeled up the label and saw a PROM and copied the data. All of the network cards would EASILY pass unit test, but out in the wild, they would fail miserably. The network card vendor came over to my friends PROM programming facility with one of the assemblies yelling up a storm, and my friend noted that "that isn't my label on the PROM, they look like this" (producing a proper one). The next action the guy did was definitely not a WTF moment, as he picked up the phone and issued an immediate STOP WORK/You're fired notice to the contract assembly house. My friend said it was a sight to see. The guy was OBVIOUSLY mad but not at him (thankfully for my friend!).
  • Curt Sampson 2009-12-18 03:56
    "From now on i am going to remove all my unit tests and replace them with comments detailing the proof of how the system is sure to work correctly!"

    Well, it doesn't work if you just do it in the comments, of course, but if you've got a good statically typed language with a reasonably powerful type system (such as Haskell, OCaml or ML) you can construct reasonable proofs that certain types of errors can't occur, and then the compiler checks that proof and refuses to compile the program if it can't verify it.

    Moving from Ruby to Haskell so I could do this reduced my testing burden considerably. I'm very pleased.

    It is, of course important to understand the limits of this technique. My compiler doesn't have a verified proof, so it might validate things that are not valid. But testing has similar limitations.
  • amet 2009-12-18 05:14
    BdH:
    Occasionally, executives do get it right.


    Really?
    So, if someone is incompentent enough to not be able do his/her job, you don't fire him/her? And instead just make that person someone else's problem?
  • Mads H. 2009-12-18 05:42
    Damn them clever u-na-versety types, always provin' stuff that don't needs provin', just more elbow grease. Good thing Robert put that fella' in his place.
  • titter.com 2009-12-18 06:44
    katastrofa:
    Gumpy Gus:
    So he proved the rest of the program, the compiler, the run-time libraryies, all the device drivers, and the OS were correct?


    Wow, that's quite a guy.


    And, oh, did he prove that his proof was correct? And did he prove that his proof check was correct? ....




    How do you test that the tests are correct?

    How do you prove that your perception of reality ("tests don't work", "code does not compile") is correct?

    How do you prove you're not just a brain in a jar talking to electrodes?

    You obviously don't understand how science works, but seeing as your nickname means "catastrophe", that's no wonder.

    But just so that you can't say I didn't answer your question:
    The tests are correct if the conditions you're testing for are covered by them.
    My perception of reality is correct if it agrees with the measurements done by other people, ideally if a causality can be estabilished. Of course, other people could also be delusional. The point is that, if everyone is delusional in the same way, then the delusion is reality, since reality is what we perceive. Of course if that is the case, you don't call that delusion. Delusion is the domain of minorities.
    I can't prove that I am not a brain in a jar talking to electrodes. That's why I don't try to. That's how science works. It doesn't talk about things that are not measurable.
  • bjolling 2009-12-18 09:00
    Curt Sampson:
    "From now on i am going to remove all my unit tests and replace them with comments detailing the proof of how the system is sure to work correctly!"

    Well, it doesn't work if you just do it in the comments, of course, but if you've got a good statically typed language with a reasonably powerful type system (such as Haskell, OCaml or ML) you can construct reasonable proofs that certain types of errors can't occur, and then the compiler checks that proof and refuses to compile the program if it can't verify it.

    Moving from Ruby to Haskell so I could do this reduced my testing burden considerably. I'm very pleased.

    It is, of course important to understand the limits of this technique. My compiler doesn't have a verified proof, so it might validate things that are not valid. But testing has similar limitations.
    You can do something similar in C# using code contracts:
    http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx
  • PinkFloyd43 2009-12-18 09:57
    You should of put it in production, after Vijay sent an email to everyone indicating that he had fixed it and if anyone had questions/issues to get with him! It's the only way to chop the head of Vijay!
  • JiP 2009-12-18 10:57
    There is a psychological condition called 'Cognitive dissonance' which is clearly in place here. Unfortunately this is often experienced by programmers. Even more unfortunately, the smarter the person in question is (often self-implicitely 'proved/n' by the level of (completed) education), the more likely it is that the reasoning will become something like: "I'm smart, so even if I do something really stupid, I can't get it wrong"...
  • AC 2009-12-18 11:00
    Jase:
    cdosrun:
    Big G:

    In case your Google isn't working:
    J Crew: Clothing for yuppies.


    I'm not sure "yuppies" will translate either. :-)

    Yuppies traditionally care more about appearance than function. Clothing for yuppies would, stereotypically, be expensive, poorly made, not last very long, and show the Logo of the designer prominently.

    I don't own any J Crew, nor am I familiar with the name, but that's the typical view of the "Yuppie" from my own culture.


    It's a bastardisation of an acronym (I can't exactly remember what for, but it's something like Young Upwardly-mobile Professional)

    Basically it refers to people who have more dollars than sense and like to show off what they consider to be their immense wealth


    Oh, so a douchebag/guido?
  • An Onimizer 2009-12-18 11:07
    justsomedude:
    In theory there is no difference between practice and theory, but in practice there sure as hell is!


    Oh dear. I'm so totally fed up with this little gem of wisdom.

    When someone quotes it to me after a WTF, it usually turns out that

    - cowboy mode was applied instead of any theory at all

    - the wrong theory was applied

    - the correct theory was applied incorrectly, e.g. due to insufficient understanding of the theory

    I have yet to meet the case where the theory was insufficiently advanced to solve the problem - in which case you should work on the theory before you try a solution.

    The above adage is just a poor attempt at being witty after having botched it, usually by people with an attitude of "Theory? We're doing real work here!" As if computers in a university and computers in an office were somehow different. The first people to make a magnetic drum memory, for example, weren't cowboys but professors, and without them the fabled garage companies wouldn't have happened, period.
  • frits 2009-12-18 11:25
    An Onimizer:
    justsomedude:
    In theory there is no difference between practice and theory, but in practice there sure as hell is!


    Oh dear. I'm so totally fed up with this little gem of wisdom.

    When someone quotes it to me after a WTF, it usually turns out that

    - cowboy mode was applied instead of any theory at all

    - the wrong theory was applied

    - the correct theory was applied incorrectly, e.g. due to insufficient understanding of the theory

    I have yet to meet the case where the theory was insufficiently advanced to solve the problem - in which case you should work on the theory before you try a solution.

    The above adage is just a poor attempt at being witty after having botched it, usually by people with an attitude of "Theory? We're doing real work here!" As if computers in a university and computers in an office were somehow different. The first people to make a magnetic drum memory, for example, weren't cowboys but professors, and without them the fabled garage companies wouldn't have happened, period.


    You win the dum-dum prize. The inventor of magnetic drum memory was an engineer and businessman: http://en.wikipedia.org/wiki/Gustav_Tauschek

    Many inventions come from industry and goverment research, not professors. See "Bell Labs". If theory were sufficient, why have theorectical and experimental physisists? Surely there is no need to test all these wonderful theories. In fact, theory only comes after making careful observations, not before.
  • Organizer 2009-12-18 11:54
    brazzy:
    Even when steel prices were highest, 150 tons of steel were worth MUCH less than "millions of dollars" (more like 20,000) - heck, even stuff that might be made from 150 tons of steel and includes a lot of energy and labor costs (e.g. a ship's engine) only has low 6 figure prices AFAIK.


    If your software bug destroys the plant, then you'll lose millions in production opportunities.
  • Organizer 2009-12-18 11:58
    JiP:
    There is a psychological condition called 'Cognitive dissonance' which is clearly in place here. Unfortunately this is often experienced by programmers. Even more unfortunately, the smarter the person in question is (often self-implicitely 'proved/n' by the level of (completed) education), the more likely it is that the reasoning will become something like: "I'm smart, so even if I do something really stupid, I can't get it wrong"...


    This is why Prolog still needs to be taught. It shows that bad premises lead to bad conclusions. Also, failed Prolog proofs can lead to infinite recursion, which smacks the point home!
  • laoreet 2009-12-18 13:36
    Shinobu:
    A proof is essentially a construct that turns assumptions into a conclusion using reasoning steps. If the conclusion is proven wrong by reality, that means one of two things:
    1) A reasoning step was wrong. I don't know how many proofs (including my own) I've sent back to the drawing board by asking the why question. Or sometimes simply: ‘Wait a minute...’ People make reasoning errors.
    2) One of the assumptions was wrong.
    And this is why I think they should have studied the proof longer. They agreed to the proof, so I assume they checked the reasoning thoroughly, which means that one of the assumptions behind the proof about how the system operates is false. In other words, the real system isn't behaving like the system in their minds.
    Now, of course I can't tell from my comfy chair what's wrong. Some people say the simulator may be buggy, but I doubt that is causing the problem. After all, it displays the same faulty reading as the real system in the same conditions.
    All I can say is that there is potentially a lot to be gained from studying faulty proofs. For example, an acquaintance of a friend of mine studies clinical trials of homoeopathy and that can teach us a lot about faults in trials and human reasoning about statistics. So don't trash proofs. They are a bit like unit tests of the human mind and you disregard them at your peril.
    The article never states that they agreed with his proof. Granted, the whole article's another bowytched job, so it's impossible to know whether they did or not, but the nearest we get in the article is a carriage return between the sentences
    While patting his notebook, he smiled and concluded, "therefore, this is my proof that the code will work — in writing!"
    and
    "Vijay,you work is quite impressive," Robert began, "but would you mind if we went over to the simulator and tried it out?"
    So, i would have to go with 2) Dog-food your own assumptions.
  • Monday 2009-12-18 15:48
    It's much smarter to try and prove yourself wrong
  • microtherion 2009-12-18 15:50
    frits:

    Many inventions come from industry and goverment research, not professors. See "Bell Labs".


    Ah yes, Bell Labs, home of Brian Kernighan (PhD, Princeton), Dennis Ritchie (PhD, Harvard), Ken Thompson (MS, UCB), Bjarne Stroustrup (PhD, Cambridge). Jes' plain folks using their gawd given common sense.

    [This is not intended to dispute frits' point, BTW, but the original article's gratuitous PhD bashing]
  • Shinobu 2009-12-19 06:25
    I think we went our separate ways much earlier: when I read ‘Vijay left Robert's ... the actual fix.’ I pictured him explaining to Robert what he had done. Then Robert's reply seems to confer his agreement.
    But you're right, that may be a false assumption, and Robert's reply may have been simple sarcasm. In which case I would want to work there even less, for obvious reasons.
  • EmperorOfCanada 2009-12-19 07:58
    The best comeback I ever heard to a guy working on his Masters in Comp. Sci. while complaining that the manager of the project had no degree at all was from the manager: "You needed someone to show you how to do this stuff?"
  • G 2009-12-19 16:04
    There is no way in known universe for 150 tons of iron, molten or otherwise, to cost "millions".

    Other than that, good story..
  • Watson 2009-12-19 23:13
    G:
    There is no way in known universe for 150 tons of iron, molten or otherwise, to cost "millions".

    Other than that, good story..
    That kind of depends on where it is and how it got there.
  • savar 2009-12-20 07:48
    <p>I am fairly confident that something like this *can* be proved, as long as every part of the system is deterministic, but I imagine the proof for something like this would be at least a few thousand pages long, unless the system is highly decoupled and you are allowed to assume perfect inputs into the component which you are working on, in which case it may only be dozens or hundreds of pages.</p>

    <p>A fun exercise at school, but completely valueless in the real world.</p>

    edit: jesus fucking christ, is there *ANY* logic as to whether the comment submission adds new lines to your post?? sometimes it does and sometimes it doesn't.
  • savar 2009-12-20 07:52

    What a peculiar thing to say, sounds to me like:
    a) The test shouldn't be written by anyone who understands how the program works 'under the hood'
    b) The testing shouldn't be done by anyone who doesn't understand the intricacies of the program
    They sound a little opposing to me....


    As long as the code is reviewed (including the tests) -- I think you're okay having the same person write the tests. If the test does something weird like inline asm to poke values in a certain place in memory, then you raise a defect.
  • Henry Elsner 2009-12-20 20:03
    Did he get paid at least?
  • Henry Elsner 2009-12-20 20:04
    Did he get paid at least?
  • BBT 2009-12-21 00:37
    Paper disproves Spock.
  • mauhiz 2009-12-21 04:59
    tantrum fail
  • BlueKitties 2009-12-21 13:19
    On one hand, I absolutely love how infallible mathematics is. On the other, I love how the Universe will occasionally say "Up yours!" and do something you never expected. I've always been torn between thinking Mathematically and thinking Scientifically. Of course in this case, I've had so much code blow up in my face I wouldn't dare put mission critical code into place without testing it first.
  • hoodaticus 2009-12-21 18:55
    I don't need a whole function to satisfy the OP's request; all I need to do is show that any one assembly instruction can be proven to be processed in a given time. Take a hypothetical instruction that requires x clock cycles and divide x by the speed of the processor. Voila! Proof.

    There are CompSci classes that test on this.
  • jw 2009-12-21 19:18
    I've met this guy. He was proud that using XP he never had to touch the mouse, at the cost of a little productivity of course, but style points count big in coding, right? Mouses are so 1989.
  • Justin 2009-12-22 08:36
    TRWTF isn't that the steel mill owner's son got to run an (I imagine very expensive) R&D lab with a good sized staff and payroll, and never produced anything? Ah well, I guess if you make a lot of money, you're allowed to do what you want with the profits, including keeping your son busy so he won't go near the production equipment


    captcha: persto (only one letter away from Pesto, which I've only occasionally not hated in cooking)
  • Suscipit 2010-01-04 05:48
    frits:
    An Onimizer:
    justsomedude:
    In theory there is no difference between practice and theory, but in practice there sure as hell is!


    Oh dear. I'm so totally fed up with this little gem of wisdom.

    When someone quotes it to me after a WTF, it usually turns out that

    - cowboy mode was applied instead of any theory at all

    - the wrong theory was applied

    - the correct theory was applied incorrectly, e.g. due to insufficient understanding of the theory

    I have yet to meet the case where the theory was insufficiently advanced to solve the problem - in which case you should work on the theory before you try a solution.

    The above adage is just a poor attempt at being witty after having botched it, usually by people with an attitude of "Theory? We're doing real work here!" As if computers in a university and computers in an office were somehow different. The first people to make a magnetic drum memory, for example, weren't cowboys but professors, and without them the fabled garage companies wouldn't have happened, period.


    You win the dum-dum prize. The inventor of magnetic drum memory was an engineer and businessman: http://en.wikipedia.org/wiki/Gustav_Tauschek

    Many inventions come from industry and goverment research, not professors. See "Bell Labs". If theory were sufficient, why have theorectical and experimental physisists? Surely there is no need to test all these wonderful theories. In fact, theory only comes after making careful observations, not before.


    Of course theory comes after. However, there are way too many coders out there who think that every problem is original, has never been solved before and needs thousands of lines in their favorite language to be half solved. They're the ones who spread that they need no stinkin theory, creating a dozen new problems in their wake for every half-baked solution they create. Well, at least they contribute to job security until the company folds. Programming failures are now estimated to cost in the trillions of dollars.

    So get a clue before you start.
  • Spudd86 2010-02-15 21:01
    arty:
    Seminymous Coward:
    Seriously, y'all are going to unanimously go with "proofs are stupid?" A real proof is a guarantee of correctness. TRWTF is abuse of the word "proof." Even an idiot can say they have a proof.


    Unfortunately, mathematics can't prove much about about complicated programs in unrestricted turing machines.

    Why don't we have standard support for making objects into communicating sequential processes in the standard library of any language? Why don't we have a finite automaton other than regex(3) in the standard library?


    Err... you can prove pretty much anything that is true about a program, finding the proof is the tricky bit.

    Luckily people can write there code in a clear straightforward manner than makes proving things about it easier (like 'the following loop invariant is maintained thus at the end of the loop we have X, this implies the next bit results in Y which is our desired result' and such). Yes, proving correctness is not easy, but doing it means you WILL find lots of errors that are hard to test for and you are forced to document your assumptions (so that if the assumptions your codes correctness and your proof rest on are false your fellow developers can point this out)

    If reliability is REALLY important you should do both testing and proofs of correctness, then follow that up with code mandatory reviews, to really flush out the assumptions and check the proof and tests and the code itself to make sure that they match each other and the rest of the program.