What Medieval Medicine and Computer Engineering have in common(blog.ezyang.com)
blog.ezyang.com
What Medieval Medicine and Computer Engineering have in common
http://blog.ezyang.com/2010/11/medieval-medicine-and-computers/
11 comments
Many software engineers don't fully appreciate how young this industry still is. We are still in alchemy times. It may be a trillion dollar industry, but it's still massively immature compared to, say, medicine, engineering, architecture, etc. We don't even have proper models and terminology to have good conversations about high-level design in many cases. When architects get together they can compare buildings structurally and aesthetically with a rich vocabulary, when developers get together to talk about software the terminology is often strikingly lacking in comparison.
Yes, this industry is still very young. Another way to think about it is that we still build software the way they built cars in 1905 - to a large extent, most products are build from scratch by hand to serve a very specific set of requirements.
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.
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.
A software product is a copy of runnable software installed on a computer. The vast, vast majority of such products are built the same way cars will be built in 2055: entirely automatically, with automatic testing and verification, with no human intervention whatsoever.
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.
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.
His mention of formal methods is interesting, because up to at least as 2000, academia has tried to instill this in their students. (Or at least tried to instill in me and my fellows.) I remember being taken to task in middle school by my instructor for writing a BASIC program via experimentation and incremental changes, instead of planning it out ahead of time. Yet, some time between my getting my undergrad degree and now, colleges started to drift away from the theoretical to the “practical” approach I’ve done since childhood, at least according to what I’ve read hear and heard about my college since.
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.)
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.)
I actually think software engineering has quite a bit in common with construction. We both work off blueprints, we have certain regulations that our creations have to adhere to, and we acquire skills as we gain experience that allow us to shortcut the conceptual underpinnings of the work of creation. A framer, for example, should have a rudimentary understanding of physics. They should know why certain shapes are strong, and how much load a given frame can bear. As they gain experience, however, they begin to recognize shortcuts. A joist in one circumstance should be 6x8", 10x14" in another. The knowledge of which implementation needs each size is not, however, rigorously determined or proven. The framer knows from experience which is required.
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.
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.
I like to read essays like that: opinionated but not ranty, well researched, encouraging discussion and engaging even for those who disagree with the author's premise. I'd like to see more submissions like that on HN and less news of the day that are going to be irrelevant tomorrow.
I think software quackery is perhaps the most easily drawn comparison here. Pick your favourite popular 'thing'; Rails, or BDD, or the grand-daddy, Agile.
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!
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!
You don't have to pay to use Rails, BDD, Agile, or other tools and approaches. Certainly there are books and courses for sale, but also quite a lot of material for free. Saying "Here's a 'medicine,' it might work for you in some circumstances, but it's certainly not always appropriate, and by the way it's free, have as much as you like," is not the promotional pitch of a quack.
One problem is just how successful 'medieval' computer programming is. A decent programmer can write software that works nearly all of the time. Very few programmers have any incentive to write provably-correct software.
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.
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.
> A decent programmer can write software that works nearly all of the time
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.
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.
One issue with software methodology assessment is the difficulty in getting consensus on ways to determine code
quality. One potential experiment I've been thinking of to work around this is by seeing if 3rd parties can tell if a methodology was used. To abuse OP's analogy of debug statements, this is essentially a "assert this practice makes a visible difference".
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!
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!
I think code quality misses the issue.
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.
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.
Bug count is a poor metric for this. Not all bugs are created equal; some have orders of magnitude more impact than others. And then there's the philosophical question about what is or isn't a "bug". Most software isn't advertised with detailed functional and non-functional requirements covering every possible use case. So if the software doesn't do something the way a user wants it to is that a bug, missing feature, or simply working as designed?
Ok, you're taking "advertise" too literally. What I meant was that software typically is thrown out to the world to serve a certain function, I wasn't making a comment on advertising materials :-).
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.
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 not a cop-out at all. The only way to precisely define "bug" in your original comment is as behavior that deviates from the specification - you need a formal definition if you want to count them. You're right that if the user says "when I click 'save', your program formats my hard drive", "yes, that is in the spec" is not really a defensible response. The user doesn't care that this is a flaw in the specification and not the implementation. But there is a huge middle ground where the specification and the user's expectations disagree (since the user didn't read the spec), and both are reasonable. Counts as a "bug" or not?
A "bug" is simply a reported issue that the developers feel must be fixed at some time in the future. It is defined just by existing in the database, and not being deferred or reclassified as not a bug. That's what I mean by bug count.
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?
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?
The only real measure is benefit - cost. Sometimes quality costs more than bugs. Take a simple editor macro. You record some simple set of actions and have the editor apply them en-mass. They may not be correct, but just getting the job done likely outweighs the faults.
According to the fascinating book "Bad Medicine: Doctors Doing Harm since Hippocrates" (http://www.amazon.co.uk/Bad-Medicine-Doctors-Doing-Hippocrat...) Doctors were doing more harm than good right up until the 1950s and some even after that due to receiving training earlier.
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.
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.
I have a hard time that a person living in the same world as me can reach such wrong conclusions.
> 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.
> 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.
I just realized that someone may be upset that I didn't give any motivation for the last statement. There are four reasons why formal proofs do not really work for computer programming:
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.
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.
Formal specifications have been used successfully. I'm reminded of this article I read:
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.
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.
We will know if it was successful when seL4 is used by someone and actually shows that it doesn't have bugs.
BTW while we're trying to climb out of the middle ages, computer engineering == building hardware, software engineering == building software.
Computer engineering is both hardware and software. Software engineering is only software. http://en.wikipedia.org/wiki/Computer_engineering
I'd still argue it's not an article about 'computer engineering'. All the references I saw were to software engineers or computer scientists.
[deleted]
In my mind, Electrical Engineering is closer to hardware engineering. I went through Comp Eng, and did many a hardware design internship, but I am quite a low-level fellow. Many of my colleagues were EE, not CE.
i think there's also a distinction between software engineering and programming lurking somewhere in the background.
I didn't like the essay much. The comparison with medeival medicine is a little shallow. One big problem he misses, is that unlike medeival medicine, computer science theory is well developed. CS has a solid theoretical foundation. The schism between engineers and academics mainly comes from the fact that "formal verification methods" are either not acheivable in practice, or require constraining a problem to a point where the verified software is not useful for anything.
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".
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".
The medieval scientists and practitioners were both rather wrong about what was going on inside. However, both computer scientists and computer engineers have a good fundamental understanding of how their systems work. If we're talking about the process of building them, then yes, I would agree, but I think its more akin to the science of management, and people like Drucker, than medieval phlebotomists.
The thing about the software industry is that we tend to support a lot of legacy stuff here, even after we have found something better. The problem here is that it's easy to learn, but it's very hard to unlearn, that's why sometimes we need generations to pass.