Kuro5hin.org: technology and culture, from the trenches
create account | help/FAQ | contact | links | search | IRC | site news
[ Everything | Diaries | Technology | Science | Culture | Politics | Media | News | Internet | Op-Ed | Fiction | Meta | MLP ]
We need your support: buy an ad | premium membership

[P]
Open Source Software, Peer Review, and Software Engineering

By _Quinn in Op-Ed
Wed Feb 07, 2001 at 05:52:49 PM EST
Tags: Software (all tags)
Software

Open Source software derives its utility from peer review, so why isn't it more common in other fields? What happens when software engineering becomes as reliable as, say, civil engineering?


One reason may be that the ethical arguments of the Free Software Foundation are particularly compelling for software developers, who then release Free (and therefore, for the most part, Open Source) Software.

More importantly, I think, is that software developers have realized that software engineering is not a mature field. My understanding of other engineering fields is that there are algorithms known to be effective whose results are provably correct, and that certification in these fields is a means to ensure that these methods are known and used by the certified engineers. Peer review is still important, because it's possible you made a mistake and didn't catch it, but it can generally be accomplished by a relatively small group in substantially less time than it took to produce the design.

None of this is true in software engineering. Academia is still working on proof techniques and has had some success in strictly limited areas; doing this `in reverse' has led to some success in generating effective algorithms for transforming (certain types of, e.g., context-free grammars) specifications (another problem -- 'building does not fall down' can be hard to prove, but can has a relatively straightfoward expansion into rigorous requirements) into software. Peer review not only becomes more important, but more difficult and more time-consuming. Conventional means of obtaining large-scale peer review (publication in a journal) can't pick up the slack for three reasons: first, there simply aren't enough journals for the amount of software produced, even if one ignores size issues; second, the journal will usually finish its peer review in about a year, which is too long for many purposes; and third, most journals aren't interested in actual code, except as illustration.

So what happens when software engineering matures? Free Software won't vanish, but I think there will be less of it: while I expect there to be more than one way to code a provably crash-proof kernel, how many times will somebody bother to prove another one? And the same ethical arguments apply. But what happens to the pragmatic cousin, Open Source? I suspect that will be determined by what happens to the software industry. Certainly, with effective proof techniques, one could imagine independent software auditing houses examining closed source code, certifying it, and sending the binaries out for distribution. How many people will want to see the source if the program never crashes? Commercial software makers are faced with an interesting problem: their product never wears out, so if they sell you one copy of a proved-correct program, why would you ever upgrade?

Well, there are two possibilities, as I see it. First, the feature war will continue, and morph in to the style war, as has happened in almost every other mass-production industry. (That is, very rarely does a single product completely dominate an industry by being 'the best'.) Or, you may see software companies accelerating two trends already in motion: customization/consulting and software rental. A company might ask its software provider for a custom feature, for which the provider charges. Or, the provider might not sell/permanently license their software: you pay a certain amount per period (per user), with the market determining feature expectations and responsiviness to requests. (That is, one provider may be less responsive than another, but charge less to compensate.)

On the other hand, this may happen without mature engineering; Free and Open Source Software continues to get better faster (in my opinion) than the non-Free/closed alternatives, draining the potential out of current business models (licensing the same software over and over again). Already, you see companies making the perspective shift to selling features or services, rather than hardware or software. Here, for example, Sun takes the position that "software is a feature." In their 1999 annual report, IBM notes that their global services division made 37% of the their total revenue, and is growing three times more quickly than hardware, and twice as fast as software.

So what changes would be unique to software engineering maturing? Once users stop complaining about reliability, what happens? Does the industry's focus shift toward customization? Toward becoming a service, like long distance? Will consumers continue to play the upgrade game, or will computing become more a tool than a status symbol? (Like, for instance, cars -- well, in the US, anyway.)

I'd expect to see an explosion in alternate interfaces and different kinds of applications, because a mature discipline should expand the realm of the feasible. I'd expect cultural changes, with more people putting more trust in computing -- especially if proof techniques extend to security. I expect, if they haven't already by then, that software patents will become much more reasonable: what is and isn't obvious to a trained practioner of the craft (e.g. `one-click' shopping) will be much better defined.

Discuss. :)

-_Quinn
Reality Maintenance Group, Silver City Construction Co., Ltd.

Sponsors

Voxel dot net
o Managed Hosting
o VoxCAST Content Delivery
o Raw Infrastructure

Login

Related Links
o Open Source
o Free Software Foundation
o Here
o annual report
o Also by _Quinn


Display: Sort:
Open Source Software, Peer Review, and Software Engineering | 32 comments (30 topical, 2 editorial, 0 hidden)
Well... (3.75 / 4) (#2)
by regeya on Wed Feb 07, 2001 at 03:34:25 PM EST

From stories friends/acquaintances(sp) have told me about their experience with Free/Open Source in TRW is that simple economics dictate such choices. For instance, and I'll be vague because I don't know how much of this I can tell, but one large company recently decided to switch from all sorts of machines to using machines running Linux for two reasons: one is that, during a presentationgi it was a choice of $1.5 million to buy 100 HP-UX machines vs. $150,000 to buy the same number of Penguin Compting rackmounts, and that several companies have started supporting Linux.

[ yokelpunk | kuro5hin diary ]

peer review vs. peer review (4.00 / 4) (#3)
by Anonymous 242 on Wed Feb 07, 2001 at 03:38:47 PM EST

I think the biggest flaw in _Quinn's essay is that he mistakes peer review for peer review.

On the one hand, there is peer review found in publishing a design or algorhythm in a peer reviewed journal. This type of peer review is great for publishing specific types of design patterns, algorhythms, etc.

On the other hand, there is the type of peer review where your immediate peer group sits down and goes over your code (or blueprints) to make sure that you haven't screwed up. This is the type of peer review that happens in good software (and hardware) companies.

Both of these are important and Computer Science (as a science) is only starting to get a nice mass of the first type of peer review. Architects, Rocket Scientists, Marine Engineers, etc. have tomes and tomes of design patterns, formulas, etc. that they can turn to for reference. "How much stress will X take in position Y if Z?" is a question that can be researched and answered within a given margin of error. Computer Science is in its infancy in providing that type of answer to many computing problems.

My feeling is that as Computer Science matures as a science, the feature war will begin to die down. Once critically peer reviewed algorhythms and design patterns become more well known and published, making a word processor, or billing system, etc. will be more a job of building out of known black boxes than the current arcane industry that is 1/4 mojo, 1/4 art, 1/4 logic and 1/4 mathematics.



Less Hurry, Less Worry (2.33 / 3) (#4)
by retinaburn on Wed Feb 07, 2001 at 03:42:09 PM EST

the journal will usually finish its peer review in about a year, which is too long for many purposes

I think the rush to get things out the door is part of the problem with software design. Im glad that GM does'nt hurray new car designs out the door in under a year. They take 3-5-7 years before a 'concept' hits the market. If we could take a slow and steady peer review approach (at least with open source) then we would find more bugs and have less 'freak' crashes and data loss.

Imagine if the linux kernel had a year of peer review (or even 3 months) before it was downloadable..sounds like a good idea.

Of course I would hate to wait for 3 months if the newest version didn't end up working ...when will they start support ENIAC !!!


I think that we are a young species that often fucks with things we don't know how to unfuck. -- Tycho


Crash-Proof Kernels (3.50 / 4) (#5)
by j on Wed Feb 07, 2001 at 03:44:33 PM EST

So what happens when software engineering matures? Free Software won't vanish, but I think there will be less of it: while I expect there to be more than one way to code a provably crash-proof kernel, how many times will somebody bother to prove another one?
To prove that a kernel is crash-proof would require the proof that it is error-free. It is widely accepted that the complete absence of programming errors can not be proven for any nontrivial piece of code.

Not exactly. (4.66 / 3) (#16)
by bgalehouse on Wed Feb 07, 2001 at 04:47:58 PM EST

Formal verification is an active field of research, and every day it goes further and further. Error-free != crash proof. 'Will not crash' and 'no buffer overflows' are much easier conditions to define formally. Error free is really quite nebulous.

Writing a perfect automated formal verifier is a lot like writing a 'perfect' optimizer for your compiler. Which is to say that it has been verified as impossible.

However, there are some very good compilers which will optimize many things very well. For the exceptional cases, you might need to get out an assembler. Similarly, there are some verifier which are pretty good, if not as good as compiliers. But sometimes you need to write proofs yourself.

But if you actually understand why a program is safe from, say, buffer overflows, then you have all the understanding needed to write a proof of the fact. Once written, proofs are easy to check; there is no problem making a computer verify that.

[ Parent ]

CS may remain immature for a long time (4.66 / 3) (#6)
by Vygramul on Wed Feb 07, 2001 at 03:47:14 PM EST

With Mechanical Engineering, the laws of Physics no longer change. We may add to our knowledge incrementally, but the general principles remain unchanged for quite some time, whereas before "physics" was often what the church decided it was; at least, in Western Culture.

With software, however, programming changes on almost a yearly basis. Look at how people programmed in 1988 compared to 1991 compared to today? We went from linear programming to object oriented programming to cross-platform OOP to Markup languages and there may not be a bottom to this in our lifetimes.
If Brute Force isn't working, you're not using enough.

a very long time (2.50 / 2) (#25)
by joto on Thu Feb 08, 2001 at 07:33:05 AM EST

Considering that object-oriented programming were invented in the 60's and your claim that people didn't do it in 1988, I would have to disagree that the practice of programming changes on a daily basis. Mostly it stands dead still. The most major change is possibly the hordes of uneducated programmers doing consulting.

[ Parent ]
an extremely long time (none / 0) (#27)
by Vygramul on Thu Feb 08, 2001 at 11:11:11 AM EST

First, I didn't say "daily" basis, but yearly. Second, just because OOP was invented in the 60's doesn't mean it was widely used, even if you yourself were on the cutting edge and used it. Look at how they taught programming as recently as 1990? There were universities still using FORTRAN as their programming language. The Internet was "Invented" <humor> by Al Gore </humor> decades ago yet it really didn't hit it big (as in popular with non-geeks) until about 1996.
If Brute Force isn't working, you're not using enough.
[ Parent ]
Unis and FORTRAN (none / 0) (#29)
by panner on Thu Feb 08, 2001 at 08:07:21 PM EST

Still using it as early as 1990's, you say? Try still using it now to teach engineering students. I'm not one, but my brother is at the University of Kentucky, and he's taking a class (I assume because he has to) to learn FORTRAN. He's got the textbook on it, and on more than one occasion, he's gone to the school computer lab to use the UNIX machines there with a FORTRAN 90 compiler (even though they have telnet and ssh access, and I hate putty under windows that he could use). Locally, I've got a FORTRAN 77 compiler (g77), and I know where to get a free (not Free) FORTRAN 90 one, but he goes to the school (not that I mind :). Personally, I think the idea is crazy, and he'd be better off with a more widely used language, but then, I could be wrong, and FORTRAN is perfect for engineering. It doesn't really matter, though, since he's in the class, and is going to remain there, I'm sure.

--
Keith Smiley
Get it right, for God's sake. Pigs can work out how to use a joystick, and people still can't do this!
[ Parent ]
yeah (none / 0) (#32)
by regeya on Tue Feb 13, 2001 at 04:27:39 PM EST

I had decided back in my CS days that I wanted to take a class in FORTRAN...I had to do some fast talking to convince anyone that I should be allowed to take an engineering class. :-)

[ yokelpunk | kuro5hin diary ]
[ Parent ]

Provably anything software is impossible (2.25 / 4) (#7)
by Luke Francl on Wed Feb 07, 2001 at 03:47:27 PM EST

I like your article, and I do thing software engineering will mature over the next 50 years or so to become a discipline of its own, but your logic has a flaw in it: there is no way to "prove" that a piece of software will not crash (or do anything else for that matter). It's equivalent to the Halting Problem, and is uncomputable. The only way to take bugs out of software is to go through the code and fix them.

Personally, I forsee a bright future for Free Software (and open source), as additional profit models besides "package software, sell CDs" become increasingly available. We've already got some companies surviving mostly on a service model while giving away their software. The Street Performer Protocol (or similar idea) could allow small, independent software developers to develop Free Software and still get paid.

software proofs (4.33 / 3) (#9)
by Anonymous 242 on Wed Feb 07, 2001 at 04:01:03 PM EST

there is no way to "prove" that a piece of software will not crash

Firstly, this is a misleading statement. _Quinn was comparing software engineering to other types of engineering. There is no way to "prove" that any given building will not collapse in on itself. There are too many environmental unknowns for this to be computed. Even the best engineered building would have problem if landed on by an out-of-control Boeing 777.

Just as tanks, cars, houses, bridges, refridgerators, etc. can be engineered to have predictable behavior within certain limits the potential is there for software to be engineered to have predictable behavior within certain limits.

Secondly, since most programming languages are expressions of logical statments, a good deal of mathematics can be applied. Source code can be audited to prove whether or not a given result is correct. The largest problem is that (in the current environment) the cost of doing so is prohibitive. Would you pay a few tens of thousands of dollars for a single license of an email program that has been proven to exhibit certain behavior? I doubt it. Very few applications (relative to the number of all applications) need this type of proof. Some do.



[ Parent ]
Dang. (3.00 / 1) (#13)
by _Quinn on Wed Feb 07, 2001 at 04:23:08 PM EST

   Someone came up with a better response to a criticism of my article than I did. This does a much better job of responding to the point than I did. Bravo!

-_Quinn
Reality Maintenance Group, Silver City Construction Co., Ltd.
[ Parent ]
you are quite welcome, send money (4.00 / 1) (#14)
by Anonymous 242 on Wed Feb 07, 2001 at 04:30:52 PM EST

I was going to write I witty response that I just realized that I issued cp -R at a directory with a symlink to a directory filled with gigs of binary files. Crud. I better go clean up before the SA starts squawking.

[ Parent ]
Almost. (4.50 / 2) (#11)
by _Quinn on Wed Feb 07, 2001 at 04:09:38 PM EST

   Proving /every/ program either halts or does not halt is impossible. However, this not preclude proving that a /specific/ program or finite set of programs does or does not halt, since that is clearly possible. (Trivial examples include empty programs and programs with only infinite loops.) This is (metaphorically) similar to how the incompleteness of number theory doesn't prevent us from proving things in it. If you really want to get ugly about it, remember that every computer is actually a finite state machine -- it has a specific and limited amount of states, defined by the amount of memory available to it (include processor registers, etc). If is theoretically (though not computationally, for any reasonable amount of memory) possible to begin at the start state, and prove that there is no terminating path in the state-graph. (Since there's a finite number of states, they can be numbered, and you can avoid infinite loops.) What this becomes in theory and engineering practice remains to be seen.

-_Quinn
Reality Maintenance Group, Silver City Construction Co., Ltd.
[ Parent ]
Realistically... no (none / 0) (#17)
by kcarnold on Wed Feb 07, 2001 at 05:09:33 PM EST

For almost all aspects of computer use, there is a simple, special case of the halting problem: the being-done-before-I-get-bored problem, which is easily checked for. Just run the program, grab a cup of coffee (or tea), come back, and if it's not done, go optimize your algorithm (unless of course you're simulating Universes, in which case you should be able to get some sort of intermediate results anyway).

[ Parent ]
correctness proofs (4.00 / 1) (#15)
by Anonymous 6522 on Wed Feb 07, 2001 at 04:31:03 PM EST

In my first semester computer science textbook there is a sidebar about correctness proofs.

To summarize it, it is possble to prove a program. You just write it down, "using the notation of formal logic" and feed it into an automatic prover. The prover generates the program as part of it's proof. This isn't feasable for large programs because it is hard to program in formal logic, and it is very difficult to prove anything but trivial programs correct.

[ Parent ]

Re: Provably anything software is impossible (4.00 / 1) (#23)
by joto on Wed Feb 07, 2001 at 08:16:55 PM EST

your logic has a flaw in it: there is no way to "prove" that a piece of software will not crash (or do anything else for that matter). It's equivalent to the Halting Problem, and is uncomputable. Yes and no!

Your statement is correct, of course, but very misleading for what people are actually trying to do.

We don't want to prove that some arbitrary piece of software doesn't crash. We want to prove that exactly this piece of software doesn't crash, which depending on what this software is may or may not be possible.

If if is not possible, then most likely the software is at fault, and actually crashes sometime. There is of course another possibility, that the software actually doesn't crash, but no one is able to understand it.

In any case, the software should be changed so that you can prove it's correctness.

.

Note that in reality, we usually try to prove that software lives up to it's specification, not that it doesn't crash, since writing a program that never crashes is very simple and doesn't require proof. Example: while true do noop; end

[ Parent ]

Software vs. cars (3.40 / 5) (#10)
by tympanic on Wed Feb 07, 2001 at 04:06:17 PM EST

I am intrigued by this article. I have an interest in software engineering methodologies, but hadn't thought about the results of better-designed products.

Something I thought of fairly early in your article (and then you mentioned it later) is a comparison to the automotive industry in the U.S. Generally speaking, cars are well-designed and reliable products. So, why do we keep buying new ones? I see two reasons.

Most obviously (to me), they wear out. Physical objects break, and eventually the owner is spending more on repairs than the car is worth. I cannot foresee this happening with software. Based on your assumption that a mature SE process will produce well-designed and reliable software, that product will just go on. From this standpoint, people's willingness to upgrade is very feature-dependant. The new version needs to do something that the customer needs, but that the old version doesn't do.

A second reason would be "coolness factor." There are many people who buy a new car every year or two, simply because they want the Newest and Best Thing. If this mentality is transferred to the software consumer, features are still the concern, but it is not so dependant on what the person needs as it is on what looks neat.

How do mature SE practices effect free or open-source software? Just because there is a way to do something that has been proven to work, doesn't mean that it is the best or fastest way to do it. Also, you cannot please all the people all the time. As in the auto industry, there will always be somebody out there who has a cool new idea on how to do something better or faster for him or her. The desire for customization, combined with continually improving capabilities of hardware will be the driving force behind new software development.

A Model T works well, but I wouldn't want to drive one to work every day.

My $0.03,
Tympanic

"I've noticed success tends to mean making sure people's expectations are low and then exceeding them" -David Simpson

Hmm.. (none / 0) (#26)
by spacejack on Thu Feb 08, 2001 at 10:02:53 AM EST

Considering the thousands (millions?) of deaths caused by automobiles every year, I would say that they have a long way to go before you could consider them as safe as software.

Anyways, IMHO (and I know this is going to piss some people off, but anyways..) the human race should not be encouraged to put blind faith in their software, open or closed (this will be tough for some to swallow, I know, as many software companies could profit immensely by doing so). I would much prefer to see people innoculate themselves against bad software by not letting themselves become too dependent on it. Why? Because most people don't know how to use or even choose software safely, regardless of how secure the software itself is. You can't force people not to buy Microsoft.

Now, there are countless exceptions to this rule: medical tech, air travel, space travel, military applications where we (for better or for worse) do rely on software for critical situations. However that software is typically being maintained by people trained to work with it -- and where the benefits outweigh the risk. Perhaps your article is appropriate within these circles.

But when it comes to the public, I think people should maintain a healthy mistrust of software and keep it at arm's length.

As far as proofs go, aren't we still pretty much cave-men in this regard? AFAIK, it's pretty tough to concoct a proof for much more than a few lines of code..

[ Parent ]
software proofs (4.33 / 3) (#12)
by rebelcool on Wed Feb 07, 2001 at 04:17:31 PM EST

all algorithms can be proven.. actually its not that DIFFICULT to do (far less difficult in my opinion than doing sentential calculus proofs...), but it does take TIME to do.

And this is where the real problem lies. What few businesses in the world that havent completely coverted to electronic systems of interacting within themselves, their suppliers and their consumers, are doing so now. It's stretching the world's programming resources. Thus things are demanded to be done fast... not giving enough time to properly demonstrate the validity of algorithms.

In some critical systems..life support machines, aerospace, nuclear plant controls..software proofs are not only common, but REQUIRED..as they should be.

However, an algorithm is only as good as its input data. But if every algorithm that handled the input data prior to the algorithm in question, were proved, then this wouldnt be a problem. In fact, a data fault could be solely blamed on a malfunctioning piece of hardware (that would be great..ever had a time when you wondered if your strangely acting cd-rom was a driver fault or a hardware one?)

In time, the enormous demand for technology workers will slow and the dumb ones will be weeded out. Then we'll all have the proper time to fix our software, and prove our algorithms. And then the world will bask in the glory of software that rarely fails.

COG. Build your own community. Free, easy, powerful. Demo site

For a bit of paranoia, from a student (4.33 / 3) (#19)
by fink on Wed Feb 07, 2001 at 05:51:38 PM EST

First of all, a disclaimer. I'm studying a Bachelor of Engineering in Software Engineering at Griffith University in Brisbane, Australia. As such, consider me "coloured" by the debate. :)

all algorithms can be proven.. actually its not that DIFFICULT to do (far less difficult in my opinion than doing sentential calculus proofs...), but it does take TIME to do.
I both agree and disagree with this statement. Algorithms, yes, can be "proven", however in reality none ever has. Think - Ok, so to prove this (warning, sloppy C-like pseudocode follows):
int i;
int j = 3;
while (i <= 3) {
i++;
}
: is fairly easy, in it's own right.

However, the following problems occur. The formal proof for the above is about 2 A4 pages of scribble - I know, I've been there. It's not pretty. :)

And that's just the beginning. Here comes the pedanticism. You then have the problem that you don't know that the compiler is proven - and no compiler has ever been fully proven to be precise. You don't know that your code, when compiled, will still work exactly as you proved it would. Then, the operating system. Can you prove that the operating system that both your program and your compiler work on, won't cause some kind of error in your code?

Now the nasty bit - at least for the hardware junkies out there. There has only ever been one proven processor - it's name escapes me for the time being - and even it wasn't fully proven. The proof was stopped after it hit 200+ pages; the processor had a very limited instruction set and was very slow. As I recall it was a project by the UK Ministry of Defence, if that helps anyone.

Proofs have been done on mission/life-critical software before. However their use is debatable; it is impressive the sorts of known faults in commonly used compilers, and in those that use it, operating systems.

It's not a matter of stupidity either. Proofs, to be proven, have to be done by hand - if you use a piece of software (Rational Rose, for example) to help you "prove" your code, how do you "prove" that your proof-generating software is precise?

So, yes, it is in theory possible to prove software. However, in reality, it takes more time than any of us have. I would recommend (it's "junk" reading but it's been good for me) the book Fatal Defect. It goes into this in enough detail to be of interest to most of us.

I still think it's something that we, as software engineers, should be working on. However it hasn't been done yet - and it needs to be done from the bottom up. Think about it for a while - can you see the catch-22? :)

----
[ Parent ]

Paranoia, why? (4.00 / 2) (#24)
by joto on Thu Feb 08, 2001 at 07:18:19 AM EST

Algorithms, yes, can be "proven", however in reality none ever has.

Oh yes, most every published algorithm featured a correctness proof in the original publication. Otherwise you would most likely not get it published in a journal.

Think - Ok, so to prove this (warning, sloppy C-like pseudocode follows):
int i;
int j = 3;
while (i <= 3) {
 i++;
}
: is fairly easy, in it's own right.

No, you can't "prove" this code. If you want to prove something about it, you must first state what you are going to prove. In other words, you need a specification. This is one of the major advantages of correctness proofs, it tends to nail the specification down correctly, at the design phase! There is great value in a specification that is both correct and complete.

In fact, most uses of formal methods are really what you would call semi-formal. You consider how to prove the correctness of an algorithm with respect to it's current specification. When you have come to the point where you think you can actually do the proof, you can stop. This might sound paradoxical, but the major value of applying formal methods is not so much the value of the proof itself, but the insight gained during the period you tried to prove it's correctness.

However you are correct, when you come down to the problem of non-proven underlying software and hardware. But the fact that hardware or software you use might be faulty is no reason to ignore formal methods as a tool. There are lots of things that can happen, that formal methods will never cover, such as faulty power lines, coke in the keyboard, earthquakes, meteorites, spontaneous existence failure, etc... As I've said, the value is not mainly in the proof, but in the process. By not using formal methods in the design, you will not gain anything but more bugs. The fact that formal methods is no guarantee against errors shouldn't stop you from doing it. Are you against testing as well?

As for your comments about not using computers for proofs, that is plain nonsense. Doing repetitive simple symbol-manipulations is exactly what computers are good at, and why we use them for automatic proofs. I would never trust a large proof written by a human, unless it had been peer-reviewed to death. Most humans make much more mistakes than computers. In any case, the current state of theorem provers make them more like proof-checkers than something automatic, unless your proof is really small and simple.

Also, an automatic theorem prover will most likely have been used in other projects, and most bugs will have been sorted out. Even if there are bugs, they will be easier to detect, because contrary to humans, who think like I do, an error in a theorem prover would most likely lead to something unexpected, at which point you will start investigating.

[ Parent ]

oops. (5.00 / 1) (#28)
by fink on Thu Feb 08, 2001 at 05:30:27 PM EST

Whoa. Forgot a </blockquote> tag? :)
Sorry, that's offtopic. No insult intended.

Sorry, might've not made myself clear. Ok, I'll try and reverse that now.

No, you can't "prove" this code. If you want to prove something about it, you must first state what you are going to prove. In other words, you need a specification. This is one of the major advantages of correctness proofs, it tends to nail the specification down correctly, at the design phase! There is great value in a specification that is both correct and complete.
My apologies. It was a bad example. What I meant was "prove" that, as a loop, it terminates - which is not what I wrote. Next time I'll take >10 minutes to write it and come up with a better-illustrating example.

Correctness proofs don't nail the specification down correctly; they aid in doing so. I know, it's pedantic, but that's just it. I've seen "good" correctness proofs which still allowed a poor specification, which in turn resulted in a defective product. I do agree, however, that a specification which is both complete and correct is one of the most important parts of a software development lifecycle.

But the fact that hardware or software you use might be faulty is no reason to ignore formal methods as a tool.
Formal methods should never be ignored; on the contrary, they should be developed further (until they are "foolproof" and "easy to use" - perhaps this is a good start for a posting of it's own?). Once again, perhaps I should have rephrased what I wrote. What I was trying to say there was that until formal methods have been applied to all software/hardware which relates to a given "-critical" product. Yes, there are many things out of anyone's control which can cause failure (as with anything humans build) and we can hardly keep track of them all. However, software and hardware does tend to have a much higher incident rate than any other recognised form of Engineering.

As for your comments about not using computers for proofs, that is plain nonsense. Doing repetitive simple symbol-manipulations is exactly what computers are good at, and why we use them for automatic proofs.
However, you still cannot prove that what the computer comes up with is correct. It is the same as any endeavour - if you used a flawed validation method, you run the risk of having a flawed product. It is simply that until someone writes a sufficiently correct validator, we must assume (strictly speaking) that it's results need some independent checks. I know, pedanticism again. :)

I would never trust a large proof written by a human, unless it had been peer-reviewed to death. Most humans make much more mistakes than computers. In any case, the current state of theorem provers make them more like proof-checkers than something automatic, unless your proof is really small and simple.
I do tend to agree with much of what you say here. There is an example used at our university regularly - that of the AECL/AECB validating a comparitively small piece of safety-critical software (about 15KLOC, in Ada, if I recall correctly) which had one purpose - shut down a nuclear reactor in the event of "any emergency". The proof was done by hand, and there was no guarantee that the proof was correct (and because the software matched the proof, there was no guarantee that the software was correct). Peer reviews still "rule the earth" and I believe they will do for some time.

However, I do disagree with your comment with respect to computers making less errors than humans. At the very best, they make as many errors as humans - after all, it is we who designed them. There are hundreds of logic faults in each of some of the most reliable microprocessors, embedded or otherwise. "Unreliable" microprocessors such as the pentium class processors have many hundreds more - and they have never been fully validated, formally or otherwise. Then you have to contend with software.

Also, an automatic theorem prover will most likely have been used in other projects, and most bugs will have been sorted out. Even if there are bugs, they will be easier to detect, because contrary to humans, who think like I do, an error in a theorem prover would most likely lead to something unexpected, at which point you will start investigating.
This, I feel, is a dangerous point of view. You would be well aware that there is always one-more-bug; it'll be that one-more-bug that catches you. It's a fine line; we can't trust humans either - perhaps using multiple independent validators and multiple independent peer reviews is the best way to validate software.

Pedanticism and paranoia may cause more stress - however if software is to be used in something that my life depends on, I like to know it is as safe as possible. We can't build redundancy into individual software units, so we need to know that our work is precise. :)

 


----
[ Parent ]

Important point above (3.00 / 1) (#30)
by wiredog on Fri Feb 09, 2001 at 08:41:44 AM EST

is that Nature Sides With the Hidden Flaw

The idea of a global village is wrong, it's more like a gazillion pub bars.
Phage
[ Parent ]

Software proofs and statistical measures (4.40 / 5) (#18)
by cameldrv on Wed Feb 07, 2001 at 05:35:22 PM EST

I think as far as software proofs go, automated proof systems are available, and can be applied to some software, but the big problem is that in order for them to work, your software actually has to be correct. The famous example of this is (perhaps someone else can provide a reference) HP using proof techniques on the design of caches in one of their PA-RISC chips. They wanted to prove that the cache never deadlocked. Even after their engineers went over it with a fine-toothed comb, it turned out that there was a condition that caused deadlock in the cache. This is the type of thing that engineers are extremely careful about from the beginning because it can be very complex, and everyone else is depending on the processors to execute their code properly.

Still, errors are found. Writing software which is correct to the actual specifications you want to achieve is very difficult and time-consuming. I'm sure that there are plenty of subtle ways to crash the Linux kernel which almost never happen, but would need additional code to make sure that they never do. Clearly one has to determine if we really need perfect software. The state of things now isn't very good. Software crashes and generally doesn't do the right thing in a lot of cases. However, There has to be a standard of "good enough."

When we buy a car we don't demand a proof that all of the systems will continue to run perfectly with proper maintanence. There is no proof because the car is not perfect. If such a thing is even possible, it would be totally impractical.

Perhaps a new agenda is in order. Your hard drive has a MTBF rating. Although it can be argued that these statistics are flawed, at least it gives you some basis for comparison. Perhaps we could create a human-based MTBF for software. What I would propose is a system that monitored software for crashes, as well as recieved user input as to any percieved flaws in the software they encountered. Then an independent body, equivalent to Underwriters Labratories, could give the software to a thousand users or so, and come up with some statistics. Ideally a single summary number would be available, as well as more detailed information as to the types of failures and the frequency.

As to getting companies to adopt this, I have no idea. Microsoft and other commercial software companies clearly have no interest in having such data published as it makes their lives much more difficult, and makes it easier for challengers to get hard numbers to back up claims as to the superiority of their software. Maybe independent funding could be obtained.

Software quality is certainly a crisis, as it is costing huge ammounts of lost productivity. However, we have to determine what level we want to support software development to cure this. It's a delicate balance, but I think that more information would help us in moving closer to it.

Remember that software is really all in the mind. (4.00 / 1) (#20)
by fink on Wed Feb 07, 2001 at 06:09:29 PM EST

First of all, here's a book for you to read. Fatal Defect by Ivars Peterson. Quite a good read, for a pulp-book, just keep in mind that it is aimed at non-techies. All the same, I think it rates up with Zen and the Art of Motorcycle Maintenance, but apparently I'm weird. :)

Now, what you say about peer reviews with respect to other forms of engineering, is not entirely true. Most - if not all, given the way engineers are supposed to work - engineers, regardless of field, use peer reviews, and most generally in design - which is almost always a purely-thought process, where little - or nothing - physical is produced.

Software, as you would be more than well aware - is purely a thought mechanism, in that it is never a physical entity (this is one reason true software engineers have a lot of difficulty with other engineers - "you don't MAKE anything!"). It is always thought. This also makes it much harder to "map" good engineering practices from other engineering schools onto software - you always end up mapping the design aspects only; software effectively stops with a "good" design.

Peer reviews, I feel, will never go away. For a start, a good proof is a peer review; a good engineer never proves his/her own product, for fear of not spotting obvious errors. Just because you can prove that what you did is right, how do you know that your proof isn't flawed? In a good proof, as with a peer review, it is done twice - and neither time by the same person.

Software has a long way to go before it can be compared with any other form of engineering (with the exception of microelectronic engineering, which is about the same age). Remember that civil engineering, in various forms, is at least as old as civilisation itself.

Here's a catch-22 too. Software, once proven, depends on a compiler, an operating system and a microprocessor. In order to build a "proven" operating system, you need a "proven" compiler - in order to build a "proven" compiler, you need a "proven" operating system. And of course, then the microprocessor comes along and screws it up for you completely. :) Even proof-software, if it ever exists, makes your life difficult - you can't write that and guarantee it's stability until you have an operating system and a compiler as "proven" technology.

I'm not entirely sure software will ever be as mature as, say, civil engineering. Software is just too complex.


----

Some thoughts (4.00 / 1) (#21)
by slaytanic killer on Wed Feb 07, 2001 at 07:19:28 PM EST

I have some issues for the people who are interested in using proofs for testing software reliability.

. A priori vs. posteriori. In terms of reliability, it seems that before a certain point, it is cheaper (time and cost) to use a priori guidelines of a program's reliability. Design and code audits, reusable proven components, etc. But past that point, it is much easier to use statistical methods to determine reliability. Testing. After all, are mathematical proofs used in determining a building's stability? No, only mathematical demonstrations. There are too many variables to consider, including quantum effects that we have no idea about. There is a combination of a mathematical sanity check and experiential rules of thumb that are used.

. Building systems to maximum reliability may be outside the scope of available tools. Civil eng is millenia old, but still there are crappy bridges and roads that need to be replaced every two years. Gathering together the best and most dedicated engineers brings these structures to max stability, but the same goes with gathering programmers to do the same.

Anyway, my thoughts on what happens after we reach Six Sigma reliability or whatever... pervasive and invisible computing. The people selling "services" will be artists and the like. Scientists perhaps as well, who pursue technologies like producing food from normal materials.

(And for a certain someone... brbrbr)

Re: some thoughts (5.00 / 1) (#22)
by joto on Wed Feb 07, 2001 at 08:04:19 PM EST

I have some issues for the people who are interested in using proofs for testing software reliability.

Nobody is interested in using proofs for testing software reliability. If we wanted to test reliability, we would test it.

We are interested in proofs for proving correctness of programs. And correctness means that on given input the program should produce the specified output. It is impossible today to take into account issues such as maximum load, run-time efficiency, and other issues that account to reliability in a proof. Proofs are not, and will never be a substitute for good testing. They are however invaluable as a design tool.

We are also interested in proofs because a provable program is a well-designed program. The simple facts that you can prove certain interesting properties about an algorithm means that you have a well-designed algorithm. If your stupid semiautomatic theorem-prover can grok it, then so can your fellow human.

Giving correctness proofs for algorithms is not something you do after you finish writing the code, it is something you do while you design the code. If you can't prove it correct, it probably is something wrong somewhere. Either try a new proof-strategy, or rewrite the program. As you will understand, this often leads to better programs.

[ Parent ]

Not only immature (none / 0) (#31)
by hardburn on Fri Feb 09, 2001 at 12:16:31 PM EST

Yes, making software is immature, but thats not the whole story. Other, more mature techincal areas (civil engineering, etc.) have rules which are based in the real world, and most of your schooling will be based on what those limitations are (i.e., how much a certian material will support, types of structures, how many people can fit through a fire door, etc.)

Software, however, has much fewer limitations. Ultimitly, the only limitations are imposed by the language (and ultimitly the machine code it must be made into). This means software has a much wider range of flexibility.

If you feel a current no language isn't good enough for a task, make a new one (Larry Wall felt this way, and made PERL). Even the limitations on machine code could be removed by designing a new processor.

There will allways be a "best way" to do something. Until, that is, someone comes up with a better way. Therefore, a heavily structured meathod of building software is not the way to go, because, by the nature of being heavily structured, it will destroy the creativity that is vital to making new and better software.

Those of you who have studied some chaos theory will note the similarities in nature's design with software. Nature always (yes, always) works by pushing things to an extreme where humans might expect them to fall apart. Instead, the resulting system is far more stable then something so heavily structured. By pushing software to a similar extreme (which Bazzar-style development does), I believe we can imitate nature's succsess.

If you don't know much about chaos theory, check out Chaos: Making a New Science

.


----
while($story = K5::Story->new()) { $story->vote(-1) if($story->section() == $POLITICS); }


Open Source Software, Peer Review, and Software Engineering | 32 comments (30 topical, 2 editorial, 0 hidden)
Display: Sort:

kuro5hin.org

[XML]
All trademarks and copyrights on this page are owned by their respective companies. The Rest 2000 - Present Kuro5hin.org Inc.
See our legalese page for copyright policies. Please also read our Privacy Policy.
Kuro5hin.org is powered by Free Software, including Apache, Perl, and Linux, The Scoop Engine that runs this site is freely available, under the terms of the GPL.
Need some help? Email help@kuro5hin.org.
My heart's the long stairs.

Powered by Scoop create account | help/FAQ | mission | links | search | IRC | YOU choose the stories!