What Medieval Medicine and Computer Engineering have in common
blog.ezyang.com
blog.ezyang.com
It seems like some kind of tug-of-war or back-and-forth is happening now between the two camps, rather than the unification the article writer seems to want or expect.
EDIT: I just realized his conclusion about the “legitimacy of complexity” is part of the problem. I read and hear all the time how clients seems to under-appreciate the efforts required to get software to work. We may never get our house in order until the outside world accepts that the profession has more in common with law or medicine than construction or plumbing. (I’m not quite clear if this is actually a problem all engineering domains have to deal with, or if it is unique to CS/IT.)
The same is true of software engineers. We gain, through experience, the knowledge as to what solutions are suitable for a particular problem. In general, however, we don't arrive at this knowledge through rigorous proofs. We arrive at it by empirical testing, and figuring out which solutions work best in a given scenario. Just as the framer is generally unconcerned with the principles of architectural engineering for the business of building a house, so too is the software engineer generally unconcerned with the theoretical underpinnings of their code when it comes to building a product. Certainly, if one is designing a new non-relational database language, or a new search algorithm, then you'd better have a very good grounding in theory. When it comes time to implement them, however, we generally accept that they are theoretically correct and concern ourselves with making it work in the real world. In the same way, a framer will generally accept that the architect knew what they were doing, and not concern themselves with the theoretical correctness of what they're building.
Admittedly OSs, compilers and frameworks are significant steps forward from pure Assembly language, but we're still a far cry from how autos are built today: automakers build a "car platform" by composing different systems, which themselves are composed of assemblies and sub-assemblies and so on. The platform is then targeted towards a specific application by bolting a car body on top, this body is usually separate from the core engineering systems of the car.
It's generally only when we are designing a new piece of software that has to handle a new set of requirements that we start building things by hand; but even then, we almost always use assemblies and sub-assemblies called "libraries" to get the bulk of the design. Then we run the design through a compiler and linker, which automatically manufactures a runnable copy of the software, and then we test it.
Mathematics builds new theorems the same way we build new software and the same way General Motors builds new car blueprints. This is likely to change somewhat as car manufacturing becomes more similar to writing software.
Now, do we have charismatic preacher men drawing up a crowd and selling their patented tonic? Does it make your dick bigger and your stories more complete? Will it put a sparkle in your eye and a boost in your conversion rate? Will it How! All for the low low price of $99.99, that's $99.99!
Does it sometimes work? Sure! Is it a sure thing? No! Is it quackery? And How!
The other problem is that I have to build software on top of buggy libraries. Even if I prove that my bit of code is correct, I might not gain much.
I sometimes hope we get to this provably-correct world, I just don't see it happening any time soon.
Perhaps this explains some of my confusion and frustration with the assertion that quality specs & designs can eliminate the need for debugging. I am still a juvenile programmer, and thus even though I have a good spec & design, my code doesn't always do what I meant it to do when I wrote it.
Have Alice and Bob sporadically use practice X on a group of changesets and track the time spent on each. Eve and other coworkers then go through the resulting list and try to determine which changesets used practice X.
There will need to be practice-specific variations of course. For example if experimenting for TDD, the changesets obviously need to include tests and code in the same commit (without indicating which came first). If experimenting for pairing, should probably report the time elapsed as the pair worked on it, instead of summing the time spent by both developers.
Just thought I'd throw this idea out here where it's somewhat on-topic and see what y'all think about its feasibility. If anyone tries this out I'd love to hear the results!
The right metric (IMO) is actually fairly easy: bug count perhaps normalized by project size or reach (number of customers). Whether the software does what it is advertised to do is the very definition of software quality. There is nothing more or less than that.
Code quality is obviously a component of software quality, but it's not the only one. In fact, there's no study out there right now (that I'm aware of) that says messy code leads to bad software quality -- just a hypothesis and lots of anecdotes. I would think that it probably is true, but it's nowhere near self-evident.
I see what you're saying, but when you build something you typically have an idea of how it'll work, even if you don't have a precise specification. My view is that if the software is of good quality, it will work like that. If it's of bad quality, it'll sort kinds work some of the time like you expected. :-)
In general, saying that certain bugs aren't really is usually a cop-out (not saying you're coping out, just that this is what I hear as a typical excuse). In industry, you're usually quickly taking feature requests out of the "bug" category very quickly, and "working as designed" is usually the result of misunderstandings, not software failure -- and is also quickly pushed out of the bug category. Anything that pings back and forth a lot is probably a result of bad feature planning, which, again, reflects on the software quality.
It's totally unambiguous because the criteria is simply that the developers in question on a particular project perceive it as a problem that needs to be fixed. Like I said, I think this is basically the definition of software quality -- does it do what it was supposed to do.
Of course, you can cheat it by having people be completely dishonest (or incompetent) about filing or classifying bugs, but that comes with the territory. We have to rely on people telling the truth and being somewhat competent in other studies as well -- there is no perfect control.
So, I stand by my assertion that trying to define a fuzzy area for bugs is a cop-out, because if it's actually fuzzy then it will be reclassified by the developers in question most of the time.
Consider an analogy that's driving my thoughts on this subject: If you have some physical product you're producing -- if issues come up that make the designers, manufacturers think about rebuilding/modifying it to address the issues, aren't those issue a problem with the quality of the original product?
Basically this changed with the germ model and penicillin (which was discovered by accident and then used by Fleming to create entirely ineffective but very profitable vaccines until one of his students, against his wishes, purified it and put it to actual use as an antibiotic).
There's some disturbing anecdotes in there, such as doctors not bothering to wash their hands while delivering babies, even after they knew it could lead to deaths, because their patients were too poor to pay for the time it would take.
Even today, it is evidence based medicine which is the new big thing. Actually testing out what works in a scientific manner with double-blind test and rigorous statistics rather than fumble through on gut feelings dressed up as science or experience.
I take comfort in the fact that while out profession is still at the quack stage, that there is something at it's core. At least we're not psychotherapists or homeopaths, though sometimes were too close for comfort.
> If a piece of code is buggy, how do you fix it? You add debug statements and observe the output, not construct a formal semantics and then prove the relevant properties.
Where does the author see the methodology of writing formal proofs used to solve problems in the real world, exactly? What I see is the first methodology ("debug statements") applied in every field of human practice with the sole exception of mathematics: you make some observations, you create an informal explanation for the observations that's the most likely (based on previous experience and knowledge of the failing system) and you either do more observations to verify your explanation of just try to fix it. If it doesn't work you try something else.
That's what medical doctors, mechanics, plumbers, police investigators, etc.
> Even the academics recognized the importance of “medieval practica; handbooks listing disorders from head to toe with a description of symptoms and treatment.”
And if my friends that study medicine and veterinary are to be believed those things are still alive and kicking.
Now, I'm not saying that medicine is still the same as it was in the middle ages (BTW 1500s is not the middle ages, the author gets that wrong too) or that computer science will never make any progress and there is no space at all for formal methods, however formal proofs is not the way most science and technology progresses, stating that is simply historical falsification.
There is an old school of thought in computer science academia that worships mathematics or actually, an idealized version of how mathematics works. It is not realistic nor applicable to the reality of computer science.
1) the fact that you wrote a formal proof doesn't mean that you proved something, proofs are as easy to get wrong as writing the program itself
2) the reason why proofs work form mathematics is that there's other people interested in reading through your proof. No one is interested in reading my proof that my code builds a valid SQL query string to retrieve some data from my own database. Even assuming that I can publish it without revealing too much about my proprietary system.
3) to prove a system correct you first need a formal specification for the system. Even assuming that you know exactly what you want the system to do, you have to get the formal specification correct, and that's as easy to get wrong as the code is. Then you go on to prove that the system is correct and it isn't. Did you get the specification wrong, the proof wrong or the code wrong? ``I have a problem, you decide to use a formal system. Now you have three problems.''
4) At this point people propose we just write the formal specification and let a magic system write the code. This system doesn't exist and we have 60 years of experience writing code that works, 0 years of experience writing formal specifications that work.
http://cacm.acm.org/magazines/2010/6/92498-sel4-formal-verif...
Unfortunately it's not freely available, but here is one paragraph from the introduction:
"Here, we report on the full formal verification of a critical system from a high-level model down to very low-level C code. We do not pretend that this solves all of the software complexity or error problems. We do think that our approach will work for similar systems. The main message we wish to convey is that a formally verified commercial-grade, general-purpose microkernel now exists, and that formal verification is possible and feasible on code sizes of about 10,000 lines of C. It is not cheap; we spent significant effort on the verification, but it appears cost-effective and more affordable than other methods that achieve lower degrees of trustworthiness."
It was an interesting article and the process they use is not typical. If I remember correctly, they use theorem proving tools, prototype in haskell, and ultimately convert that to C. They claim that Haskell seemed to save them time and their man-hours ultimately were similar to other more traditional micro-kernel efforts.
Edit: That said, if it is indeed practical to do this, it is only on a small subset of programming work, at least at this time.
Edit 2: I found a version that is freely available: http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
I'm not sure if it is exactly the same as the ACM piece, but it is very close.
Formal verification requires "ground truth". Something external that defines what the program should do, exactly. That's possible in some cases (a CPU emulator, for example, can be verified against a physical CPU). Most of the time, however, that doesn't exist.
That means what's usually necessary is a formal description of a formal semantics. Those things, almost universally, require either creating a Turing Complete semantic description language (to allow the semantics to be rich enough to express the solution), or a verry simple problem domain.
In the Turing Complete case, the formal spec degenerates to the program. That leaves you in a case where you are proving that the program does what the program does, which is useless.
The problem with simple domains is that they violate the law of leaky abstractions. All abstractions leak. Simple domains can rarely solve real problems. This is true even for cases like bison and flex. There is a reason most compilers use hand written parsers: they need to be usable by people. Once you move away from "I want a Boolean function that says if string S is in language Y" to "I want to provide usefull error output that helps people figure out the mistakes they have made, and I want to provide contextually relevant assistance in authoring code" the formal model falls apart.
So my prediction is this:
"Attempts to raise the level of abstraction (provided it's possible to escape to lower levels), will succeeded. Formal verification, however, is a myth".