A famous term coined by EwDijkstra
. It means:
- Every programmer has to be able to demonstrate that his program has the required properties.
This is the central idea of all of Dijkstra's work on computer programming.
To what extent is this principle compatible or incompatible with TestDrivenDevelopment
(TDD)? Dijkstra encouraged a logical/mathematical kind of "proof", where the party arguing for correctness had to demonstrate step-by-step that the implementation was sound. In contrast, TDD reverses the burden of proof -- the assumption is that the implementation is correct unless someone can provide a test that proves otherwise.
It's incompatible because tests always only cover a small sample of your program, they don't prove your entire program is correct. Extreme logical reasoning about a program can prove it is correct, whereas tests only cover small samples of the program functionality. However in practice, testing is useful because bugs in programs do exist, despite all our logical reasoning. When a bug is found in software, it is useful to keep the tests available for future use to ensure that bug doesn't crop up again (RegressionTesting). I think unit testers see software as engineering (engineers like to test), whereas Dijkstra definitely wanted software programming to become a mathematical discipline (math equations can be proven wrong much more effectively using logical reasoning on paper, rather than testing millions of parameters as inputs)
I think most people will agree that formal proofs of correctness are not feasible for the complex systems we build today. But has TDD gone too far in the other direction, saying basically "If it works, then that's GoodEnough
; we don't need any deeper understanding than that?"
I want to mention that my reading of Dijkstra's ideas is that he didn't mandate formal proofs of correctness validated by proof checkers. He knew the limitations of the technology. So while I can't speak for Dijsktra, I would assume that for practical software building he would have agreed that proofs might be informal: imagine for example in a peer review of your work, you'd have to convince the (reasonable but inquisite) reviewer that your code is correct. More importantly he emphasized the requirement that your design of the program should be driven by the proof that you have in mind.
[This page was about Prof Dijkstra and requiring proofs (if not formal proofs) for correct program code. If you look at the Wikipedia article on him, you will see that he valued Math above CS and wanted CS to become more of a Math sub branch. My 35 plus years of experience tells me that everything I have read about Mr Dijkstra was naive and misguided. Some would say "Who cares?" but I would say that this Math emphasis is not benign. It is harmful to our field and holds back the progress of real CS. see FacultyOfSoftwareEngineering
. --- DavidClarkd
I'm sure that in the long run, he envisioned better language design and more importantly better development education (he characterized the software engineering discipline as "how to program when you can't"), that will make formal proofs a reality. There's no substantive evidence other than the typical naysayer's mumbling that his vision is not achievable sooner or later. And should I mention, Dijkstra contributed a lot more to our profession than all his naysayers combined. -- CostinCozianu
[You make an all encompassing statement about the merits of Prof Dijksta as compared to all other "naysayers" (you must be a Mathematician)! Would you care to enlighten a mere professional programmer as to how his entire, long career could be incorrect while a professed Mathematician is correct about a field he never actually worked in? We all want better "language design" and better "development education" but do you really think that will come from the people who don't actually develop anything? When was the last time that CS professors actually asked professional programmers what they want for tools or what techniques actually worked or didn't? Why don't these professors ask what areas of language design research would benefit or enhance the work that these professionals actually do? --- DavidClarkd
Another thing I want to mention, is that Dijkstra spelled out what we all have in mind more or less. I think that when we write down some code, we all are are at least partially "convinced" in a corner of our mind that "it should normally work", in other words we already have some partial proof or some sketch of a proof in mind, otherwise we wouldn't write that code. He only asked for a bit more rigor and intellectual discipline in the way we do it. I don't think that's such a tall order, that we can refuse a priori to follow his model.
The above sounds like a lot of pandering to a Mathematician pretending to be a Computer Scientist without any argument. How many and how big were the computer projects that were successfully designed, implemented and used by end users that were written by Prof Dijkstra?
He taught computer programming without actually knowing "for sure" how to program himself because he wasn't a professional programmer. How does that make his "theories" about programming valid? You wrote "I don't think that's such a tall order, that we can refuse a priori to follow his model.". Show me some evidence that would make such a statement worth "believing or following until proven wrong"!
What is wrong with designing code by playing around with different ideas until the spark of a solution emerges? What is wrong with imagining a solution and then verifying the unknown parts needed to fulfill that vision before solidifying your design? I could go on but there are many useful ways of designing programming systems that meet many of the goals of software development like maintenance, speed, flexibility, speed of creating etc that have nothing whatsoever to do with Math theorem proving.
No human can possibly do a walk through of code and be any near as thorough or fast as the CPU of the computer can. In the end, if you disagree on the validity of the code with the CPU, you automatically lose! Stop the desk checks and use the power of the CPU! If you can't show an example of how a program will produce erroneous output, given data from the domain defined by the program specification, then that program is probably "good enough" until you can. If you end up with a "bug" the world won't end. Fix the bug and move on. Only ivory tower persons can spend unlimited time, producing Mathematical proofs while the real world just keeps moving on.] --- DavidClarkd
Large (or relatively large) information systems, though often business-critical, are not life-critical. Cost/benefit analysis on them shows formal verification is not worth the expense. For relatively small, life-critical systems -- firmware of drug delivery systems or heart pacemakers, weapons systems, aircraft navigation and autopilot systems, nuclear reactor control systems, and so on -- formal verification is worth it and provides added assurance of validity.
The examples you give are obscure and very few in number compared to all programming projects. I don't think Dijkstra's ideas were intended for such a small group of programs. Like all Mathematicians, he wanted to make statements that would encompass all
cases when the world of creating programming, is not homogeneous. There is nothing stopping any programming project from spending whatever time they think wise, in testing and showing that their project is without bugs. No special "formal verification" is required in the general case and many methods of ensuring "bug free" code are available, in the exceptional cases. Dijkstra specifically recommended "code walk through's" which my 35 plus years of experience as a professional programmer/developer, tell me is a waste of time. My disagreement with this idea from a professional Mathematician still stands.
This is just another case of a Mathematician pretending to be a Computer Scientist and in Dijkstra's case, he was very convincing. Who could imagine that the extremely important task of teaching programming would be given to people who have never been professional programmers? Should the blind lead the blind? --- DavidClarkd
- Eh? You don’t use an informal proof or walkthrough to show that your multithreaded or distributed application works as intended? How do you test for deadlock or starvation?
[I am currently finishing a computer language/system that is designed to be inherently distributed and does automatic concurrency using multiple real threads and any number of green threads as well. This isn't the place to explain "deadlock and starvation" but I can tell you my solution had nothing to do with "informal proofs", Math, or walkthroughs.]
Code walkthroughs and formal verification are not the same thing. Whilst I don't doubt that Dijkstra would have encouraged a more formal approach, or at least more rigour, in programming than the ad-hack approach that many programmers take, I'm sure he would have recognised the practical unreasonability of doing it on every program. That doesn't mean it's any less a good idea. If we could automate formal verification and do it with reasonable resource consumption, there would be no reason not to do it.
By the way, all computer scientists are mathematicians. Not all programmers are mathematicians or computer scientists.
- Well what is your solution, then? Come on man, don't hold back. [I have a link to my website and an email address on my user id. I have lots of "not quite complete" documentation there and I would be happy to answer your informed questions by email or on MaxOopsRelational. DavidClarkd]
This is your
opinion and definitely not a fact. My BSc degree has a mayor in Computer Science and a minor in Math. I have had a very long career in applications, tools and designing/creating computer languages. I have used very little Math in all the hundred's of thousands of lines of code I have designed and written. Most of my code has been written using the tools I created myself. I have studied, contributed and hopefully still expect to contribute to the "science" of making computers more useful, through better software tools. Although I know quite a lot about Mathematics, I certainly am not a Mathematician. Are you saying that my practical contributions are worth less than the Math algorithms that constitute the unused but published papers of our "so called" CS professors? I do agree that not all programmers are computer scientists. I also would add that some Mathematicians have become true computer scientists but then so have trained chemists etc. Mathematicians have no special place in CS and because they dominate the publicly funded CS positions at Universities and teach programming that they don't do professionally themselves, there should be a heaping dose of condemnation toward the CS pretenders in our field. --- DavidClarkd
You are a software engineer, not a computer scientist. Computer scientists contribute greatly to the theoretical and mathematical underpinnings of computing. Software engineers contribute greatly to applying computing to real-world problems. There is no reason for computer scientists to castigate software engineers, or for software engineers to castigate computer scientists. They are two sides of a computational coin.
Again, this might be your opinion but definitely not fact. Very few professionals call themselves "Computer Engineers" [I meant Software Engineer, my mistake] because designing and creating software isn't an engineering type discipline. If you had enough experience actually solving real world problems with computers, you wouldn't make such an unqualified statement.
That's a curious assertion. What do you believe my experience to be?
By the way, I call myself a software engineer, and I continue to develop software even though much of my current career focus is on developing and maintaining university courses that teach computer science and software engineering.
[I only did some tutoring of 2nd year CS students, for the course I passed with a challenge exam. I have had a micro computer career that spans 38 years with over 100,000 lines of assembler coding/design, to hundreds of thousands of lines in C, at least 15 other languages, created a language/database that sold over 30,000 copies, worked on projects for over 65 companies and designed/programmed over 1,000 application projects, big and small. I am the first one to say I learn new things every day, but I am not happy when people question my right to call myself a Computer Scientist.]
[I took a 3rd year course, in 2000, in "Software Engineering" and (at least from this course) it looked to me like the SE crowd wanted CS to revert to some kind of Math. Good luck with that! CS has transformed our society over the last 40 years like nothing else has. Every advancement in almost every field can be tied to computers and the software that run them. Almost all popular and currently used languages and tools are made by companies or crowd sourced rather than by academics. All this good has been gifted to Mathematicians that have publicly stolen what rightfully belongs to others (public payed positions at Universities in the CS department). If CS professors are doing research in Mathematics, then the Math facility should be footing the bill, not the CS department.]
Computer science researchers are doing research in computation in all its myriad forms, but computation is fundamentally mathematical. I know there is pure mathematics being done in computer science departments, and applied computer science being done in mathematics departments. That's probably why so many universities combine math and computer science into a single department. It sounds like you're bitter because the course you took wasn't what you expected. That happens -- take another course. SoftwareEngineering encompasses a broad spectrum from purely theoretical computer science at one end to totally empirical pragmatism at the other.
[Actually, I think CS professors should take a course from me! Who knows, maybe they would learn something.]
[I don't think that "computation is fundamentally mathematical"! I think computation is based on what set of instructions a computer can execute. Why would you call a branch or subroutine call Math? The exact configuration of constraints that software developers have to solve their problems with is defined by the arbitrary set of features embodied by the CPU. This isn't Math. If some people want to adapt some Math notions to these things, as Math is a kind of language, then good for you but that doesn't make programming, some kind of Math.]
Just a few quotes from the Wikipedia article on Prof Dijkstra:
- One starts with a mathematical specification of what a program is supposed to do and applies mathematical transformations to the specification until it is turned into a program that can be executed.
- Dijkstra eschewed the use of computers in his own work for many decades.
- Even after he acquired an Apple Macintosh computer, he used it only for email and for browsing the World Wide Web
- Much of Dijkstra's later work concerns ways to streamline mathematical argument.
[Does this sound like a Computer
Scientist to you? If he called himself a "computing scientist" which was a branch of Applied Mathematics, you might have a case. The person described by these quotes obviously wasn't interested (or knowledgeable) about how solutions
are encoded in computer programs
, under the constraints of real world CPUs
, to solve real world problems
.] -- DavidClarkd
exactly like a computer scientist to me.
[How can someone so obviously "anti" computer (and pro Math) call himself a "Computer Scientist"? Leaving out 1 word out of 2 is ok with you?]
Computer science is the study of computation in all its myriad forms, which includes what was Dijkstra's area particular interest, the mathematics of computation. Dijkstra wasn't "anti-computer", he was a theoretician; he simply wasn't that interested in the application of theory. Likewise, most astronomers are interested in stars, galaxies and planets; they aren't that interested in telescopes. The desktop computer is only one possible implementation of the theoretical foundations of computing, and for those who are concerned mainly with the theoretical foundations, it is not of particular interest. Yet, without those theoretical foundations, we would not have computers.
[I guess we can agree to disagree. I think someone who is only concerned about Math is a Mathematician. Someone like me is concerned with computers and the software that runs on them, therefore I call myself a "computer scientist". Your analogy about studying a telescope is the same as studying a computer, is nonsense. The telescope might be comparable to the designer of a CPU but not software designers. I also have created many "theories" and then tested them by actually creating the code and having the CPU verify my "theory". I have also had many theories about how "end users" actually use code and this has made me design many enhancements to the UI of my programs. Most of the "theories" I have conjured, have had everything to do with "Computer Science" and very little to do with Math. If I was a designer of a CPU, then I might need a theory of computing but my expertise is in creating useful software and the tools that make that process better. Although I am not an expert on what it takes to create a new CPU design, I have read the things that Prof Dijkstra "invented" and they have nothing to do with computer design or anything I have ever used. I think your opinion on the merit of his contributions aren't supported by the facts I have read about Prof Dijkstra. If you believe that the theory (Math?) comes first and then the design and implementation in software design, you don't know much about software. I programmed over 100,000 of assembler on a Z80 CPU running at 2 megahertz. It had a 16 bit address space and no segment register. The 8086 (which came after the Z80) still only contained a 16 bit address space but also included a segment register. This gave it the ability to access 20 bits of address space (on 16 byte boundaries) and that was enough memory space to start the explosion of PCs. What Math theory was it that invented segment registers? Could have just been a common sense solution to the problem of providing more address space while still only using 16 address lines?] --- DavidClarkd
"Very few professionals call themselves "Computer Engineers" because designing and creating software isn't an engineering type discipline."
Actually, very few professional programmers call themselves "Computer Engineers" because that term is already in use for those engineers who design computer hardware. The appropriate term is "Software Engineer", of which I am one.
If you feel so strongly that computer scientists are all mathematicians, why not call it computing science and make it a branch of the Math department? Statistics is a branch of Math that contains mathematicians so why not computing science as well?
There are people who actually know what tools and techniques work in programming computers so why not have them teach these things to tomorrow's programmers? Where should research that makes better computer programming tools and techniques be carried out? What faculty do you suggest? Why should the future of computer languages (operating systems, etc) be held hostage to the profit/loss of private companies? Is there no public interest in better programming tools and better education for the people that are making our way of life so much better?
If the research that people like me need, can't be done by the CS departments, then in what department should it be done and what would you call it? Remember that hardware design and electronic devices using computers are created by Computer Engineers, so that name is already taken.
I wouldn't say you are not a "software engineer" so why would you say that my self designation of "computer scientist" is incorrect? A fact and your opinion aren't exactly the same thing. My definition of a "computer scientist" is my opinion and not stated as a fact. I am well aware of who currently hold positions in CS departments and the kind of papers they publish. I just wish and argue for it to be otherwise.
I prepared a new page to answer my own question. FacultyOfSoftwareEngineering
At the university I went to, statistics wasn't part of the mathematics department.
They are being taught. Wherever there are people and the equipment and the desire to do so. I have no suggestions here. It's not. Yes, there is.
What research do you need done, and why would it need to be done in a particular department?
[There are people who actually know what tools and techniques work in programming computers so why not have them teach these things to tomorrow's programmers?]
They do. I do. My colleagues do.
[If you are a professor and don't have at least 10 years experience as a professional programmer, then you don't! -- dfc]
I have about 30 years experience as a professional programmer. Most of my colleagues have at least 10 years professional experience in IT, and some have more experience as a professional programmer than I do.
[Where should research that makes better computer programming tools and techniques be carried out?]
In companies, in universities, and by every working programmer with an interest in making better computer programming tools and techniques.
[What faculty do you suggest?]
Does it matter?
[I think it does matter and I prepared a new page on this topic FacultyOfSoftwareEngineering
. -- dfc]
There are faculties of software engineering. I work in a School of Computing & Mathematics, with a strong focus on software engineering.
[Why should the future of computer languages (operating systems, etc) be held hostage to the profit/loss of private companies?]
It isn't. Note how the future of operating systems, for example, appears to be firmly in the hands of the OpenSource community. There's more Linux, and Linux derivatives, running right now than anything else. Every popular programming language has significant OpenSource implementations that are available for free.
[Database facilities dropped from languages so that Microsoft and Oracle get rich! Microsoft's operating system is "open source"? Apples front end is "open source"? What percent of desktops do you think are Linux, excluding Android phones, servers and hackers, of course! Of course C++, C#, Java are all open source, right? Is OpenSource
helping or hurting CS languages by making them essentially worth nothing and putting the money in database managers and operating systems?]
Open source is unquestionably helping the industry in general, by sharing code instead of keeping it proprietary. That means the real marketable value is the programmer who can produce code, rather than the code itself. By the way, desktops are the only computing area where closed source operating systems still hold sway. On mobile, embedded and server platforms, no. And, yes, C++, C# and Java are all open source in the form of (for example), GNU C++, Mono, and OpenJDK. Not sure what you mean by, "Database facilities dropped from languages so that Microsoft and Oracle get rich."
[Have you actually developed software then marketed it to thousands of users? I have. Even though I will concede that a few open source projects have been successful for a few software developers, most software created is either created for a company on a proprietary basis or it's use is licensed while the code is proprietary. When I talk about software, I don't talk about embedded systems, games, phone apps etc. The vast majority of designers and programmers work for business and most of those people don't use open source. Some, like Google have taken advantage of open source to create proprietary code for themselves. Google extensively used MySQL internally for many years. Google still uses an optimized version of Linux for it's massive server farms.]
Yes, I've developed software and then marketed it to thousands of users. I was a founding partner in a small Canadian software company -- specialising in custom and vertical market software -- from the mid 1980s to about 2000, when I retired from full-time management and development and moved to England and academia.
[Open source is a silly quality. Who would put the time and effort into changing the source code of such massive and complex code without getting paid for it? I have been a professional programmer for more than 35 years and I would never download the source for Linux, make my own changes, and then rely on that code to look after my files and programs. I have used Linux as a web server for 13 years but I have never downloaded anything but a binary image.]
Open source doesn't mean you have to modify the source, only that you can if you need to. More importantly, it associates value with programmers, rather than with programs.
[Foxpro was a very fast language that contained many database facilities. It later allowed most SQL commands to be executed directly on it's tables without extra licencing or cost. You could mix your program code and database as you wanted. Microsoft bought that company in the 1990's and then discontinued it's development in 2007. I believe it was because, using FoxPro
, you didn't need to spend thousands for Microsoft's SQL database. What other class of software has created the billions that databases have for Oracle or Microsoft over the last 10 years? --- DavidClarkd
Foxpro's biggest limitation was that if you used its built-in database engine, you were constrained to unscalable and insecure file-based database sharing, and it lacked transaction processing. If you used external DBMSs, then you didn't gain much from the Foxpro language that you couldn't do as easily with Delphi, VB, Java, C++, C#, Python, PHP, etc. It was discontinued because its market need was addressed by MS Access.
[Is there no public interest in better programming tools and better education for the people that are making our way of life so much better?]
There are hundreds of thousands of us, maybe millions, working on precisely that.
[Paid by who? In your spare time? Is this what will take our tools and techniques to the next level?]
Paid by our employers. In many cases, it's paying us directly to develop better programming tools and better education. I am paid precisely for that. In some cases, it's paying us indirectly, by paying us to work on <x> so that we have enough money to spend time working on <y>.
[I wouldn't say you are not a "software engineer" so why would you say that my self designation of "computer scientist" is incorrect?]
Because what you describe fits popular use of the term "software engineer" better than it does "computer scientist".
[My comments weren't about popular opinion, we both know what that is, rather I was talking about what should be. In general, professional software people don't have "designations" other than general University Degrees and therefore can call themselves what they like so long as they can justify that designation to the people who will hire them.]
If you're talking about what should be, rather than what is, please make it clear.
[You might have misunderstood what I said above, I agree that some of what you say is popular opinion but that doesn't make it true or legitimate. I had a partner for almost 10 years who was a world famous Mathematician and I can assure you, I know the difference between a Mathematician (my ex partner) and a Computer Scientist (like me). If you look up logical fallacies, you will find that popularity has no bearing on the truth or falsehood of a statement.]
Indeed, popularity has no bearing on the truth or falsehood of a statement, but neither does your desire for "the truth" to be something other than what it is. Why do you want to call yourself a computer scientist, when everything you've written above and on FacultyOfSoftwareEngineering points to the fact that you are the very essence of a software engineer? Leave the computer scientists to their thing; you and they have no quarrel unless you want to make it into one.
I don't think Mathematicians pretending to be Computer Scientists are benign. They promote and study Math and I promote and study Computer Science, so you are wrong that I am a SE. I invent, not just apply what I know about CS. As I have already stated, "Engineering" as defined by "Civil, Electrical, Computer etc" is the practical usage of well known systems and ideas
. That isn't what I do and not what other software designers and developers do either.
First: I think the current group of pretending Computer Scientists are getting public funding and recognition based on the achievements of others, who are getting neither of those things from the public.
Second: It is very difficult to hire programmers who are worth hiring because they are being taught by people that aren't professional designers and programmers. Should the next batch of Accountants be taught by people that are Economists? I think there is nothing wrong with Economists but they shouldn't be teaching accounting at the highest level! I think it is only accidental that Mathematicians know much about programming and the tools that facilitate software development.
I believe the future of software development has been critically hurt by these Mathematicians and our field will continue to be retarded by continuing with the status quo. It is also extremely unfair to the legion of "the best problem solvers" the world has been seen, to give their just deserved credit to Mathematicians. --- DavidClarkd
Can you provide evidence that "the future of software development has been critically hurt by these Mathematicians" ... "pretending to be Computer Scientists"? It sounds to me like your beliefs are shaped by dystopian fantasy rather than reality. For example, I don't know of any "pretending Computer Scientists [who] are getting public funding and recognition based on the achievements of others" nor do I know any self-described software engineers who are not also innovators, inventors, and researchers. Finally, whilst I've no doubt that some education is suspect, and there are undoubtedly programmers being taught by individuals who have never professionally programmed, I doubt it's any different from any other field. There are chemists being taught by people who have never worked for chemical firms, and mechanical engineers being taught by people who have never hefted a wrench or used a lathe. In my experience, however, the majority of programming professors and lecturers are ex-industry professionals who are so enthused with programming that they feel compelled to share their knowledge of the craft with those who wish to learn it.
Your comment implies to me that you haven't read much of what I have wrote on this topic.
I've read enough of what you've written to get the gist of it, but as you're neither a recognised authority in the field nor do you cite recognised authorities and your claims do not accord with my experience, I'm afraid I can't give you much credibility.
1. Have you looked at the papers that are published by so called "Computer Scientists"? They are all Math papers! If not all then most are Math papers.
2. How much language and tool research is done in academia that is actually used by real programmers and designers? I suggest not much.
3. I have first hand knowledge of a world class Mathematician who was my partner for almost 10 years.
4. I met and talked with many other professional Mathematicians.
5. I took many Math courses when I went to University.
6. I talked to CS professors and took 2 courses in 1999-2000 that were called CS but were actually more Math from professors that were Math professionals rather than CS professionals.
7. I have continually read and kept up my software and industry knowledge over a long career of over 38 years.
8. When I first went to University and took CS, my professor was a Math prof who learned enough CS to teach the next lesson. Non of this was his fault as he was originally forced into the job. I knew more in 6 months about CS than he did (not his fault).
9. Over the years, I have hired programmers (more than 1) who received a CS degree with honors that couldn't program even the most simple of tasks.
10. My experience tells me that most CS professors have got a doctorate where their thesis looked more like a Math paper and then got a job as a professor without any real world experience. Even if that is no more than 50% of CS professors, there is no criteria for professors in CS to actually have a certain about of real world experience.
My evidence is that the only real useful research in CS is and has been done by companies rather than academics for at least the past 30 years. Show me where all the millions of public money spent on CS research has made the tools of CS better in that time period?
Rather than my beliefs being shaped by a "dystopian fantasy", I would say your comments say you don't have a clue what you are talking about. Funny, but you seem to be the one calling me names, defining what I am, and talking down to me. I won't be responding to any more of your comments on this post as you just aren't worth the effort. --- DavidClarkd
Actually, I do know what I'm talking about. I've read hundreds, maybe thousands of academic papers by computer scientists. Yes, they almost invariably include mathematics, because mathematics is a crucial means for ensuring rigour, and computer science is a mathematical science. I've read few papers that are pure mathematics -- though some are -- but they are almost invariably related to computational theory. Yes, there are computer science graduates who can't program, but there are also mathematics graduates who are superb programmers. I've hired both.
You appear to be sounding off over some grudge, or relating very narrow experience, but not presenting reality.
I said I won't respond anymore BUT I found a link to a "Computer Science" researcher at IBM. Check out this link. http://www.scott-a-s.com/cs-is-not-math/
When someone simply says 'computer science is math,' they are doing a disservice to all of these other fields in the discipline that are clearly not just math. Of course, we use mathematical reasoning whenever we can, but so does all of science and engineering. Math is the common language across all empirical disciplines, but they do not all tell the same story.
This is just a sample quote from his blog post. --- DavidClarkd
Well for this little programmer, the proof is in the application. Whatever the mechanism for proving the system, the purpose of proof is satisfying the requirements and having no manifest bugs. -- ChaunceyGardiner