So I think the problem isn't money; the real problem is there just isn't enough software! We have a software deficit. With software being a critical part of nearly every business in the world, there is huge demand but massively insufficient supply. In my industry, there are only two big software providers and a handful of smaller ones. And it's a huge industry in both money and sheer size. But they literally cannot buy anything but big balls of mud.
People are paying big money and small money for whatever software they can get. And that natural consequence is that performance, reliability, and security are hit or miss.
They might not get it, of course -- the money is an (often ineffective) stand-in for institutional/organizational change, AKA "throwing money at the problem."
It's simply easier to get people to spend gobs money than to change their comfortable short-term habits. (Evidence: Wasted gym memberships everywhere.)
The lack of discernment of the buyer is creating all this software waste. This is one of the reasons that MS Excel and Access run most of the world's financial data. The format is open enough that it basically imbues the user partial programming ability without having to worry about things like new line feeds and uptime.
Painfully true. There are techniques for writing better software. They work. They take longer and cost more. They are not widely used outside aerospace.
In general, the answer typically involves formal specification and formal methods that check the code against these specifications, combined with testing and coding standards that result in analysable code.
More references:
https://www.cs.umd.edu/~mvz/cmsc630/clarke96formal.pdf
http://research.microsoft.com/en-us/um/people/lamport/tla/fo...
There's also various specification languages for multithreaded behaviour, which allows you to analyse your programs behaviour using software tools, for example SPIN[0].
For example, with MISRA it may be C, but feels like Ada.
Or Spark similarly for Ada
It's unfortunate, and it's sad to say I'm often part of it at some level (but I fight it dammit!).
I asked him, as delicately as I could, what had happened.
This project we were working on, he told me, had been going on for about half a year, and during that time there had been a meeting every week, where everybody involved in the project had an opportunity to get together and review and discuss the progress of the project.
So there was this guy, who had only attended the very first of these meetings, without saying a single word. And the week before the thing is supposed to go live, he shows up again, with a long list of changes he wants to make to the application.
Needless to say, that programmer, and several other people in the room, told that guy how he had six freaking months to tell the programmers about his requirements, and the he could not possibly expect them to make all these changes a week before the application went live.
So that guy goes to the highest-ranking manager involved with the project, manages to pull some political strings, so that manager goes to this programmer's boss, that boss goes to the programmer and tells him, "I know how much it sucks, but you have to do this. I share your pain, but I, too, am powerless to refuse this request."
When building material things, it seems, houses or ships or airplanes or railraods or whatever, people do realize that you cannot tell, e.g. the construction company that you actually want a house with a circular outline rather than the rectangular one the company has been building for the last, what?, three months. Managers at car companies, I guess, do not storm into the engineers' offices a week before production of a new car starts to tell them the vehicle not only needs to be small and fuel efficient, but also needs to be able to work in antarctic climate and run on carbon dioxide instead of gasoline.
With other products - at least, that is the impression I get - people have an intuitive or explicit understanding of the limitations of the things they want to have built, and they also seem to basically understand that you cannot make drastic changes at the last minute. With software, which does exist in the tangible way that, say, a car our house does, people seem to have a much harder time understanding those limitations. I am not sure this is the entire problem with software development, but it is a big part.
I recognize some organizations will not accept that answer and will try to make me take the blame. Such organizations will tend to have a very poor tech department.
For instance, it's easy to prove that there's an infinite number of prime numbers. There's no biggest prime, because if there were (hand-wave proof coming) you could multiple them all together, add one, and have another prime number. Easy right?
Now tell me if there's also an infinite number of twin primes, ie pairs of prime numbers separated by two.
Here's a good xkcd: http://xkcd.com/1425/
Maybe not as much as people think. There are machine-assisted mechanisms for building mathematically perfect software. See Curry-Howard oriented languages like Coq and Agda. It's certainly harder to write perfectly, provably correct programs, but maybe not as hard as most people think.
There is also a lot of middle ground in the form of relatively powerful (but not quite Agda-powerful) type systems.
As for type systems, mission-critical software has generally made good practice with them (Ada, proof checkers, etc.) More so than consumer and enterprise circles. Yet a ton of catastrophic bugs have been the result of errors outside the scope of type checking, and as a counterpoint, our telephony is pretty robust with dynamically typed Erlang switches. It seems that mechanisms for building self-healing and concurrent systems are often put aside and equivocated solely with strong type systems. From what I recall, Erlang's signature feature of hot code loading actually conflicts with static typing.
How so? The implementation is not the specification; but the type is the specification. Like people like to say, the type is a Theorem, and the implementation is is the Proof of the Theorem. (In a very real sense.) And don't you need both?
Hopefully there can be some type inference at a certain scope, to avoid cluttering the code with a lot of 'obvious' type declarations. I forget exactly how dependently typed languages work in that regard right now (there certainly can't be full type inference).
> All the compiler does is checking that these two specifications are consistent with each other.
"All". That's already better than informal mathematical proofs.
> Your types can have bugs too, in which case nothing will help you.
Yes, just like any other kind of alternative specification there is. Short of mind reading, there is no getting around actually describing what we want. But where there is a distinction to be made is in what kind of specification is easy and declarative enough to use as to give the least likelihood of introducing bugs in the spec itself.
> What frustrates me about detailed type systems is that as detail increases, difficulty of writing the types will increase and type bugs will become more common.
I guess if we assume that we have collapsed/unified the type and term(/value) level, we can use any old Good Software Engineering Practice when it comes to keeping the types tidy. Like using type functions to encapsulate some of the detail: maybe have a `sorted(list)` function instead of having to write it out each time we need it.
This is just a guess though; I don't know how the dependent programmers do it. Well most of what I'm writing here is guessing, on some level.
(And judging by the pride that some people show when they proclaim that "half of our code base consists of just tests", well... I certainly think that types can be more succinct than that!)
> Now, assuming the bugs in your code and types are statistically independent that would still save you a lot of bugs, but I suspect they are not.
I guess if we go with the previous assumptions of a unified value/term level, then the statistical chances are the same in that types are just ordinary values, instead of the types belonging to its own language. ;) Then we just have to make sure that the amount of types is substantially smaller than the amount of "regular ol' code".
Typer er fremtiden. Håper jeg (kanskje).