Business is another thing, nobody convinced them to go along with anything, it's the other way around. Incentives to produce software the way it is produced actually come from businesses as they are the ones paying for it. Engineers just go along with it.
I get that software industry is very dogmatic and it's hard to see things for what they are. But we should at least try.
I'm using "correctness" to mean software that is bug-free.
The system that the software is a part of may still have problems, but none of those problems should be caused by bugs in the software components. It's also possible to build bug-free software that solves some other problem than the one you have. Both of those issues are orthogonal to the issue of why the industry doesn't adopt methods that generate bug-free code.
> Yours is just one such method, and one of the expensive ones.
I expect to be able to train normal, non-programmer folks to be able to use it (a HOS-like system that permits elaboration of a top-level spec into bug-free working code) to develop bug-free programs. If that works it may be so cheap that it depresses the market for "real" programmers. I should be so lucky.
But regardless, these methods (HOS, Cleanroom, etc.) just aren't that dreadfully expensive. And bug-free code, once written and paid for, can be reused. The cost analysis has been on the side of "provable correctness" for longer than my lifetime.
> This is very important distinction if you want to understand why "proving correctness" cannot get anywhere.
Well I don't accept your assumption that '"proving correctness" cannot get anywhere'. My whole point it that it has gotten places and we're all ignoring it because we prefer to use e.g. C and Java and {{POPULAR LANGUAGE}}...
> For a lot of software even if we need reliability there simply exist more objectively better ways to achieve it.
If you are talking about "reliability" of software I don't know what that means other than bug-free.
I know you can build reliable systems out of unreliable parts, but to do that there still has to be some reliable system orchestrating them and compensating for failures.
But again, I'm not saying there's a method for reliable systems, only reliable software. The absence of the former doesn't invalidate the existence or desirability of the latter.
> Business is another thing, nobody convinced them to go along with anything, it's the other way around. Incentives to produce software the way it is produced actually come from businesses as they are the ones paying for it. Engineers just go along with it.
The "suits" aren't to blame for this one. They only know what we tell them (to a first approximation.) If you tell your boss, "I can chop better with this ax than that chainsaw." you're lying or ignorant. How is management supposed to even know the possibility is there if the programmers doesn't tell them? Or they bring it up and the response is "Sure, I'd love to use {{TECH}} but {{EXCUSE}}."?
There's a cost for bugs. If you can get bug-free programs for the same upfront cost as buggy ones (and my whole argument is that we can, but don't) then there's no upside and only downside to accepting buggy software, and methods that permit buggy software to be written.
We could use chainsaws, instead we use axes and claim chainsaws are too expensive and axes cuts fine.
It's not because the bosses, who only care about board-feet[1] per worker per hour, are too cheap to buy chainsaws.
[1] "The board-foot is a unit of measure for the volume of lumber in the United States and Canada. It is the volume of a one-foot length of a board one foot wide and one inch thick. " ~https://en.wikipedia.org/wiki/Board_foot
I do get the point of your analogy, but it's really a very poor analogy.
> If you can get bug-free programs for the same upfront cost as buggy ones (and my whole argument is that we can, but don't)
This sounds like a massive market opportunity. One then wonders why absolutely no one has exploited the opportunity. There's something missing here.
As an example, here's a way to get Logical Paradigm programming in your favorite language http://minikanren.org/ It's simple, easy to understand and implement, and you can use it to do things like type inference and type checking with flexible and powerful constraints to define and ensure invariants and stuff like that. This stuff isn't expensive or even that challenging, we just don't do it.)
Here's Edsger Dijkstra debunking the books written about HOS.
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...
An evaluation by the US Navy concluded. "the HOS literature tends to advertise their ideas and products more than making a contribution in substance to the field of Computer Science. The author recommends that USEIT not be used in the TRIDENT program or any program development at NSWC. Even for a high level system specification, USEIT is not seen as a good choice. A mathematical functional notation or a PROLOG-like notation appears better suited for that purpose. The examples in the Appendices of this report, especially Appendices C, D, and E, show that a LISP-style mathematical notation is more compact and normally easier to read than the control map notation of USEIT. On a more positive note, the author considers the functional approach to system development and programing very promising. Systems so conceived and programs so constructed are more amenable to analysis and therefore, in principle, more reliable and better manageable."
http://www.dtic.mil/dtic/tr/fulltext/u2/a198753.pdf
So are we just talking about functional programming when we say HOS? If so, the pros and cons of functional programming have been discussed at great length.
Here is an interview with Simon Peyton Jones (one of the creators of Haskell) talking about why Haskell is "useless". It's a short interview worth watching if you want to understand the nuances and challenges and costs around creating high quality and bug-free software.
All of human history is a tire fire then. Most stuff around the world is poorly engineered and just gets the job done. Wooden bridges with rope and wire holding them together and no analysis whatsoever done on what load it can bear. For most of history those bridges made up the majority of the bridges in the world. And it worked just fine until modern transport put higher demands on bridges. Yet, you still find clunky wooden bridges all over the undeveloped world, and they continue to work.
Should we try to do better? Of course we should. But someone has to pay for it. It doesn't happen magically.
Regarding the Toyota Unintended Acceleration bug, that's gross negligence if the top priority coming from management wasn't quality and if someone can prove that, they should end up in jail. And I would not excuse the developers either. I would never ship code that I know might kill someone. I would rather quit and work as a cashier. Please re-read my original post because I never said quality isn't important. I only said that quality is not always a top priority, and that in some cases it should be a low priority. A website for a 2 week marketing campaign will never kill anyone. It would be a waste of resources to insist on anything other than just shipping it once it works.
If you're honest with yourself and look around, you do it all the time in your own life too. You draw a diagram on a piece of paper or a white board to explain a concept and then you throw it away or erase it. You don't carve it in stone just because it will last longer and someone a hundred years from now might find it useful. You put up a simple rope barrier to keep people from stepping on newly planted grass. You don't erect the wall of China. Temporary "low quality" solutions that will later be dissembled and thrown out (or save the rope for reuse at least) are often the best fit based on the requirements.
> You just have to use the right method (which has existed for about 30~40 years, nearly totally ignored.)
I'm very skeptical that markets would completely ignore an opportunity to beat the competition if the costs were exactly the same but the results were higher quality. But I'm going to look into this. Thanks for the reference. I'm going to read James Martin's book and see if I learn something new that will help me write better code.
Yes. (We have spent the last 10,000 years recovering from the Younger Dryas and we are only just now getting back on our feet. Heck, most of us still think agriculture is a good idea when really it's about the dumbest way imaginable to relate to the soil. But I digress.)
> Most stuff around the world is poorly engineered and just gets the job done. Wooden bridges with rope and wire holding them together and no analysis whatsoever done on what load it can bear. For most of history those bridges made up the majority of the bridges in the world. And it worked just fine until modern transport put higher demands on bridges. Yet, you still find clunky wooden bridges all over the undeveloped world, and they continue to work.
Ah, but none of those bridges are built out of electrified math.
Software is electrified math and it can be perfect.
And it's self-referential: we can write perfect meta-code that emits only perfect code.
> Should we try to do better? Of course we should. But someone has to pay for it. It doesn't happen magically.
My point is not that we never try. My point it that the world contains many attempts and most of them have been ignored by most working programmers.
> Regarding the Toyota Unintended Acceleration bug, that's gross negligence if the top priority coming from management wasn't quality and if someone can prove that, they should end up in jail. And I would not excuse the developers either. I would never ship code that I know might kill someone. I would rather quit and work as a cashier. Please re-read my original post because I never said quality isn't important. I only said that quality is not always a top priority, and that in some cases it should be a low priority. A website for a 2 week marketing campaign will never kill anyone. It would be a waste of resources to insist on anything other than just shipping it once it works.
Let's assume, for the sake of argument, that I'm wrong and correct software always costs more than incorrect software. In this scenario (which may well be the REAL scenario) you have put your finger on the important bit: we're talking about the location of the inflection point.
Allow me to reference Randall Munroe, "Is It Worth the Time?" https://xkcd.com/1205/ It's a handy chart that shows, "How long can you work on making a routine task more efficient before you're spending more time than you save? (Across five years)"
It's not precisely what we're talking about, but it's got the same flavor: how much do you expect to use the buggy software vs. the cost of correctness...
Now my point would be: The industry should have had a house-on-fire urgency around reducing the cost of correctness to shift the infection point downward so that all but the most trivial software can be made correct economically.
We should have been doing that since forever (or at least sometime after the Apollo 11 mission.) Instead we generally ignore these sorts of things.
> If you're honest with yourself and look around, you do it all the time in your own life too. You draw a diagram on a piece of paper or a white board to explain a concept and then you throw it away or erase it. You don't carve it in stone just because it will last longer and someone a hundred years from now might find it useful. You put up a simple rope barrier to keep people from stepping on newly planted grass. You don't erect the wall of China. Temporary "low quality" solutions that will later be dissembled and thrown out (or save the rope for reuse at least) are often the best fit based on the requirements.
Have you been to Daiso? It's the Japanese dollar store. Pretty much any human problem that can be solved by ten ounces of plastic can be solved in Diaso for $1.50. I'm not generally into consumer culture, but I love Daiso.
You don't need 'temporary "low quality" solutions' if you have Daiso.
It's not that I don't use hacks, or don't respect them, it's that we're so far behind where we should be in terms of off-the-shelf solutions (to programming) and we don't seem to be quick on the uptake...
> I'm very skeptical that markets would completely ignore an opportunity to beat the competition if the costs were exactly the same but the results were higher quality. But I'm going to look into this. Thanks for the reference. I'm going to read James Martin's book and see if I learn something new that will help me write better code.
God bless you! (I collect powerful ideas and I cannot tell you how many times people have said, "If $FOO is so great, why doesn't everybody use it already?"... I don't know! I don't freakin know! It makes me sad. All of human history is a tire fire, indeed.)
- - - - - - - - - - - - -
This is my reply to your later comment on this same thread.
First, wow, I'm impressed. You are actually doing the homework and I tip my hat to you with great respect. Seriously, that's the nicest thing you could have done and I really appreciate it.
Second, yes the language and presentation around these "HOS" ideas has apparently always been really bad, with the issues you describe. It also doesn't help that the necessary background knowledge and jargon wasn't wide-spread at the time.
Third, yes it was panned by Dijkstra and the Navy, I've read both of those reviews, and their objections are not without merit. But, and I say this as someone who has huge respect for Dijkstra, they were both wrong: they both missed the fundamental advantages or "paradigm", if you will, of how HOS et. al. works.
(Also, have seen that Simon Peyton Jones interview. And no, we're not just talking about Functional Programming, that's kinda orthogonal. E.g. Haskell helps you write code with fewer bugs, HOS prevents them in the first place. Another way to differentiate them is that if you're typing text in a text editor to make software you're not doing HOS regardless of the langauge.)
So, poor marketing, bad reviews, obscure principles and the general disinterest of industry led to this powerful technology languishing.
Yet, I insist there's something there. Let me try to convey my POV...
In modern terms I can describe the crucial insights of the HOS sytem concisely. Here goes:
Instead of typing text into a flat file of bytes and hoping it describes a correct program, the HOS method presents a tree of nodes that is essentially an Abstract Syntax Tree (but concrete and there's no driving syntax because there's no source text.) The developer edits the tree using only operations that maintain the correctness of the tree.
This is like "Par Edit"[1] in emacs, or a little bit like some of what J. Edwards is attempting with Subtext[2], or the old "syntax-directed programming environment called Alice"[3] for Pascal. (Again, it's not that no one has ever tried anything like this, my whole point is that powerful techniques for writing software with fewer bugs in have been around for a long time and we, in general, don't use them.)
The main difference from these is that HOS uses a very simple and restricted (but Turing complete) set of operations to modify the tree: Sequence, Branch, Loop, Parallel. (There are some "macros" built out of these operation for convenience but underneath it's just these four.)
Starting with a high-level node that stands for the completed program you gradually elaborate the tree to describe the structure of the program and the editor/IDE enforces correctness at each step. You literally cannot create an incorrect program.
Apparently normal people, accountants and such, could sit down in front of the IDE and,with a little training and coaching, learn to describe their own work processes in it and essentially write programs to automate (parts of) their own work.
I've been working towards bringing this to market, on and off, for years now. In fact, my first programming job was the result of a talk I gave on a prototype IDE at a hacker convention about fifteen years ago. I have just finished implementing type inference and type checking for my latest vehicle: a dialect of the Joy programming language. It has been slow going (I lead a chaotic life) but I'm on the cusp of having something I think will be really great. If it works, it will revolutionize software development.
Quixotic, I know, but somebody's gotta tilt at those windmills...
Anyway, thank you again for taking the time to look into this. I can't tell you what that means to me personally. I know the "Provably Correct" book is terribly written, but I urge you to try to look beyond that. All I can really honestly tell you is that I'm convinced there's something really important and useful there.
[1] "ParEdit (paredit.el) is a minor mode for performing structured editing of S-expression data." https://www.emacswiki.org/emacs/ParEdit
[2] http://www.subtext-lang.org/
[3] "In a syntax directed editor, you edit a program, not a piece of text. The editor works directly on the program as a tree -- matching the syntax trees by which the language is structured. The units you work with are not lines and chracters but terms, expressions, statements and blocks. " https://www.templetons.com/brad/alice.html
Interesting discussion. Thanks. I will keep my eye on this space from time to time.
I disagree strongly. I would say that software development is a tire fire. Every day there are reports of bugs in software causing all kinds of real-world problems. These days software bugs can kill people[1]. And there are only going to be more CPUs and more software and more bugs going forward.
> Markets have already mostly figured out the rare cases when such robustness is really needed.
I don't see how this is a supportable statement in a world that includes the "Toyota Unintended Acceleration" bug? (Among so many many others.) When you say, "a perfect solution according to markets is the solution that does the job for the lowest cost over time" aren't you effectively saying we should only expect software to be as good as has to be to protect the liability of some corporation? Not to take a cheap shot, but uh, I think the families of the people who died in the car accidents-- excuse me, collisions ("'Accident' implies there was no one at fault.") --might have a different attitude to software correctness?
In any event, your entire argument is predicated on the idea that correct software is expensive. But this is only true because we, as an industry, have not made effective use of the the available tools to write correct software!
It's not expensive to write correct code. It doesn't take longer either. We just don't do it.
Dr. Margaret Hamilton figured out how to write bug-free software as a side effect of her work on the Apollo 11 program years ago and nobody noticed.[2] (She's the person who coined the term "Software Engineer" BTW.) Byte-for-byte, flawless code is no more expensive than buggy code. And maintenance costs are near zero, so it's actually cheaper. You just have to use the right method (which has existed for about 30~40 years, nearly totally ignored.)
Please PLEASE don't make excuses. We've can get this right, even if "the market" doesn't notice or care.
To reuse my lumberjack metaphor from my other comment: Chainsaws exist. They are safer and faster than axes. There is in fact no way that cutting down trees with an ax is objectively better than cutting down trees with a chainsaw.
You are maintaining that, since trees are felled well enough with axes today, there's no sense in investing in chainsaws and chainsaw training, not now, nor ever in the future.
You're saying that "the market" only really needs wood cut by axes and doesn't value wood cut by chainsaws because all the furniture made with it is good enough, and we should just live with splinters and chairs that break and drafty houses, etc...
Frankly, it's kind of a lame argument to find on a pro-tech forum. Fancy sophisticated technology is awesome, unless it threatens to obsolesce your favorite ax, eh?
> you have to be able to find qualified developers, and what developers learn is based on popularity and fashion.
This is the source of the problem: we're not "engineers", we're not even car mechanics! We're barely above the level of kids building go-carts in their backyards out of junkyard parts. We should be ashamed of our fashion-driven-ness. The amazing thing is that we got the business people to go along with this![3]
Maybe someone should just start offering chainsaw-cut wood at cheaper prices than the hand-hewn crap and see if "the market" likes that noise? (In case I'm being too arch, that's exactly what I'm about right now. I'm so freaking passionate about this.)
"Program correctness" shouldn't have to be "top priority" because it should be the default. You should get it "for free" along with the software for the same price because it costs nothing extra.
[1] For example: "A Case Study of Toyota Unintended Acceleration and Software Safety" Prof. Phil Koopman. September 18, 2014. Carnegie Mellon University https://users.ece.cmu.edu/~koopman/pubs/koopman14_toyota_ua_...
[2] Nearly nobody noticed. I know it sounds crazy but it's true: There's a simple, easy method to develop bug-free software. James Martin wrote it up in a book "System design from provably correct constructs: the beginnings of true software engineering." in 1985. That's probably the best source if anyone wants to read up on it.
[3] A programmer in language or framework A who cannot or will not learn language or framework B is not a good programmer. (I don't mean putting "Won't do PHP" on your resume, I mean that you can't or won't learn it in the first place.) Q: "What if we can't find Python devs? There are so many Java devs. We should use Java." A: "Why would you hire a Java guy who can't do Python? Even to do Java?" I've had that conversation a bunch of times.