NASA’s Mars Climate Orbiter was launched on December 11 1998 with the ambitious mission of studying Martian climate; the cost of the program was more than $300M and a good share of it was allocated to development of the necessary software. Unfortunately, as the Orbiter was approaching the red planet it vanished and it did not take long for the monitoring scientists to realize that it was gone forever!
The reason behind the failure of the orbiter was a very simple software glitch. Instead of calculating a specific metric in newtons the program was using pounds omitting a single call to a conversion function; a code bug that could have been fixed with a few characters of code were enough to destroy the space program and invalidate all the hard work of thousands of the most qualified scientists and engineers worldwide!
Mars Climate Orbiter is just one of a very long list of projects that failed due to an extremely silly programming mistake; it can be used as another example that verifies the fact that proving any piece of software to be completely bug free and fully tested consists an impossible task.
Even the most extensive testing suite, represents an extremely limited subset of all the possible paths that any application is expected to have thus it is simply impossible to believe that in any way we can “prove” it error free with a guaranteed behavior complying to a specific set of rules!
Given the fact that the verification process is asymmetrical to its falsification, induction cannot “prove” anything; although a billion successful tests cannot prove the validity of an application, a single fail is enough to designate it as invalid! The problem lies in how to discover the failing conditions of course and nobody can be sure that they do not exist since it is impossible to test all the possible combinations of variables and execution paths.
Despite the huge record of failing applications caused by simple “bugs”, many software developers insist that they can deliver flawless and completely bug free applications!
Whenever I hear something like this, I am sure that it represents the view of a junior and not very talented programmer who sounds like a salesman trying to please the ears of his audience!
One of the most critical skills of a software developer lies in his ability to decide that the incompleteness and inefficiency of his code has reached a level that will be tolerated by its clients. Although this statement might sound provocative and strange, it also hides the secret of success behind any kind of software that can be developed! Software engineers, developers and project managers who claim that they are striving to deliver bug free and fully functional code are either lying or simply do not know what they are talking about.
I have heard several developers and program managers bragging for the obvious (but also impossible) goal of fixing all known bugs as quickly as possible and never release the next version while all fixes are committed! This approach is nothing else than wishful thought or a marketing motto that might be used to convince some MBA manager who also knows very little about the creation of software.
Setting aside very trivial cases, the complexity of any piece of software that exposes any level of useful functionality is such that even the larger quality assurance and testing teams can never verify its validity to its full extend. The responsibility of the senior programmer is to make a successful judgment call, deciding that the solution has reached a level that can be deployed to its users with reasonable completeness and robustness! There is little doubt that users will later discover some of its bugs and feature shortcomings and some of them will become the fixes of the next release; great software relies on periodic piecemeal releases which are fixing existing bugs and add new features based on user feedback.
Shooting for perfection delays dramatically code delivery and in many cases make it impossible. One of the main reasons behind failing projects has to be attributed to inexperienced program managers who fail to understand that software development is neither an exact science nor a logical structure that can be validated using some kind of a mathematical procedure. Software development instead, involves a great deal of talent and intuition, resulting to a mix of science and art with the artistic component playing the major role in most of the decisions to be made.
I need to clarify that by no means I consider an advocate of sloppy releases or have the intention to convert end users to beta testers. The point I am trying to make is that no matter how mission critical the software can be and how important the problem it tries to solve, it has to become crystal clear that it is simply impossible to reach a level of guarantee bug free solution. Regardless of whether it is an automated trading system, a nuclear reactor protection system or an android game, at some point somebody has to decide that the software is ready to be shipped to its users! Deciding that the software has reached an accepted level of completeness and its bugs are tolerable is one of the most critical judgment calls that a developer is asked to make.
It is up to the understanding of the senior developer to decide whether his program is ready for delivery and this is the skill that will separate him from the crowd more than anything else.
PurposefulPhp seems like an interesting idea although I need an example of its use to fully understand how it fits in the contract description. When you say Contracts as code (instead of contracts plus code) I assume that you mean to decouple declarations from definitions. If this is the case how your approach differs from IDL? Is the only difference that your framework is PHP specific or it also proposes some additional features?
Functional languages are approaching computer programming using a purely mathematical approach. The problem with this approach lies in the fact that although mathematics consists an analytical propositions (meaning that essential all math is build on top of logic) computer programing needs both analytic and synthetic approaches as it solves empirical problems rather than pure a priori defined propositions.
The fact that your friend claims that he can “mathematically prove” the correctness of his service means that he is viewing it as an “analytical” rather than an “empirical” procedure thus his proof is just a tautology that restructures the a priori conditions that are considered “correct” in an axiomatic fashion.
An empirical statement / solution can never be “proved correct”; all it can done with it, is to validate that it passes all the related tests that we can think about.
Thanks for letting me know. (No exclamation point here).
Empirical and synthetic can be used as synonyms in this context.
We can also prove analytical statements as they are confirmed by logical rules (for example Euclidean Geometry). Synthetic or empiric statements can never be proved. The can also be validated and eventually falsified (for example Newton Laws).