A small British firm shows that software bugs aren't inevitable (2005)
spectrum.ieee.org
spectrum.ieee.org
"I was shocked to learn that the binary search program that Bentley proved correct and subsequently tested in Chapter 5 of Programming Pearls contains a bug."
That's from Joshua Bloch's discovery in 2006 that Java's binary search implementation was broken: http://googleresearch.blogspot.com.es/2006/06/extra-extra-re...
Arguably addition (or any operation) that overflows with signed integers ought to cause some kind of SignedIntegerOverflow exception. If you want to do modulo mathematics in the set of [0, 2^n) then you should explictly use unsigned integers, which are defined to work that way.
So you could have "integer, range [a-b), exception on overflow" or "integer, 32-bit, unsigned, wrap" or "integer, 8-bit, signed, saturates" (the latter is useful in codecs and often available in assembly).
def sum(a, b) when is_integer(a) and is_integer(b) do
a + b
end
def sum(a, b) when is_list(a) and is_list(b) do
a ++ b
end
def sum(a, b) when is_binary(a) and is_binary(b) do
a <> b
end
sum 1, 2
#=> 3
sum [1], [2]
#=> [1,2]
sum "a", "b"
#=> "ab"Are there any restriction on what the code in the guards can do?
But the guard code are just macros, so... ;)
But I do believe that Erlang underneath does have actual limits.
Yes, ranges work. They (and ordinary integers) throw exceptions on overflow:
type NonoverflowingByte is integer range 0..255;
type OverflowingByte is mod 256;
For saturating arithmetic, there doesn't seem to be built-in language support. (There isn't even a standard library package. That seems to be a bit of an omission. Isn't saturating arithmetic common in the kind of real-time environment where Ada is used?)
Ada so totally deserves to be better known.
I do wonder why it isn't. It's probably handicapped by its history: once people have written off a language they'll never look at it again, despite improvements to fix the very problems they fled.
As an Ada advocate, what does it do badly? String processing? Networking?
String processing is both really nice and a pain. Built-in strings are fixed size, but the `array<>` magic means you do string processing using functional style without needing to explicitly size anything. The string libraries are a bit of a mess, with `Wide_String` and `Wide_Wide_String`, because they made the same mistake as Java and Windows about UCS-2 vs Unicode.
The standard library is mostly really cool, but it makes the same mistake C++ does in that entries in collections are always initialised by copying, so you can't have collections of non-copyable objects. I forget the details but I think the last time I tried to do collections of pointers I couldn't make it work properly.
Ada's generics are awesome. Nested functions that work properly are awesome. The compilation time is awesome. Access semantics that prevent you leaking pointers to inner stack frames are awesome. in-out parameters are awesome (they mostly replace pointers). Being unable to pass a nested function to a procedure as a callback parameter is less awesome; the access semantics forbid it.
To my mind, though, the biggest showstopper in Ada is a technically fairly trivial thing: it's case insensitive. This means that any programmer used to case sensitive languages, which is basically any programmer, will have to drastically revamp their coding style to work with Ada, because none of the usual conventions about separating locals from globals by capitalisation work any more. It also makes Ada code look ugly to the untrained eye. It's hard to convert people when the first thing they say when looking at code is 'ugh'.
Cool breakdown. This isn't true anymore in C++11 with move semantics.
Also the expression functions only being in module specifications is probably due to their source code being needed to inline them.
Don't remember how it handled overflow.
We can only work with the tools and techniques we've discovered so far. Later, we find situations or results that show our tools or techniques aren't correct or aren't good enough and we improve them to cover the new situations.
It would manifest itself with 32-bit integer indexes and with arrays of greater than 2^30 elements. So phooey. You can't even fit that many array elements into a 32-bit address space. And if you're in a 64-bit address space, you should be using 64-bit indexes.
Whine: way back in the 1960s, the IBM S/360 threw a fixed-point overflow exception (okay, to be pedantic, they called it a "program interruption", but it's the same idea) when you did that. Sadly, the Fortran compiler of the day masked it. And this same philosophy has carried over to today. About 99 times out of 100, fixed point overflow is bad, why is it being masked off?
Would this mean that Bentley's proof was in fact incorrect (i.e. not a valid proof at all) or that it simply didn't consider integer overflow for fixed size ints?
I wonder to what extent the implementation (i.e. the size of the integer type used) should affect the proof that an algorithm is correct?
Inside a formal system it's relatively easy to understand what's going on; the real difficulties are at the boundaries: how do we build a formal model of a real system, and how do we translate formal results back to the original system? It's a lot like programming: manipulating data is easy, the problems are getting the right data and interpreting what the output means.
In this case, the model didn't capture overflow; so the proof is valid for that model, but it's not a useful model for Java's ints.
Getting that correctness to propagate because of the strictness of all the tools involved and accuracy of their construction is the issue, which leaves us with needing to either automate proofs with Coq or prove things in more general ways that lead to undecidable problems etc. Still, the fact that one function can be written bug-free and known to be bug-free does indicate that it's not an inevitability of probability playing out as code grows.
We have null-pointer exceptions and no maybe type. The API's that emit nulls sometimes make me expect sewage to leak from light sockets. It's possible to do better. We just don't, and none of us love it. Rust and Kotlin are at least very exciting. I'd like to understand some Coq more in the context of x86. What routines are strictly necessary to even do Coq? A response based on some statement about how the Y-combinator enables X where X leads to Y would not surprise me.
No they're not, since you can't nest NULLs.
Say I have a database of "Users", with "birthdates" mapping a "User" to a "DateOfBirth" and "spouses" mapping a "User" to a "User", I can look up a User's DateOfBirth either using a Maybe or by allowing NULLs:
-- Maybe
getDOB :: User -> Maybe DateOfBirth
-- Nullable
getDOB :: User -> DateOfBirth
-- Maybe
getSpouse :: User -> Maybe User
-- Nullable
getSpouse :: User -> User
-- Maybe
spouseDOB :: User -> Maybe (Maybe DateOfBirth)
spouseDOB u = fmap getDOB (getSpouse u)
-- Nullable
spouseDOB :: User -> DateOfBirth
spouseDOB u = let s = getSpouse u
in if s == NULL then NULL
else getDOB s
- `Nothing` indicates that we can't find the spouse
- `Just Nothing` indicates that we can find the spouse but not the DOB
- `Just (Just x)` indicates that we found both the spouse and the DOB
In the nullable case we can only distinguish between two kinds of values:
- `NULL` indicates that either we couldn't find the spouse or we couldn't find the DOB, but we don't know which
- Anything else indicates that we found the spouse and the DOB
The Maybe approach gives us strictly more information; although we can choose to ignore it if we like, either by using `join` or by replacing `fmap` with `>>=` (AKA "bind", which is a combination of `fmap` and `join`).
Your nullable example is better compared to this, which also discards the required information:
spouseDOB :: User -> Maybe DateOfBirth
spouseDOB u = case getSpouse u in
s -> getDOB s
Nothing -> Nothing
DateOfBirth* spouseDOB(User& user) {
Spouse* spouse = getSpouse(user);
if (spouse)
return &spouse->dateOfBirth;
return NULL;
}
Exactly. Your version is just doing what `join` or `>>=` would do, which I mentioned at the end; ie.
mySpouseDB u = fmap getDOB (getSpouse u)
-- Using join
yourSpouseDOB u = join (mySpouseDOB u)
-- Using >>=
yourSpouseDOB u = getSpouse u >>= getDOB
Of course there's nothing magic; `Maybe` just increments types. I was phrasing myself in the context of a language like Java, which has NULL but no pointer manipulation.
In a language that lacks maybes, but has nulls, what is the equivalent of the type Maybe (Maybe Int)?
> Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.
Even ignoring the lack of composability, flatMap is an operation on a broad category of which Maybe is one example; that generality is a key part of its utility. ?. is a special-case operation on nullables, if you want to use it on any of the other things that flatMap works on (e.g., lists), you need a different operation, so you can't build generic algorithms. So, its not substantively the equivalent of what Maybe provides in languages where maybe is part of some broader category of operations on which flatMap can be applied.
int **
While it's certainly part of it, I would disagree that it's the key part. The ?. operator is flatMap in the context of Maybes, and Maybes alone are useful for preventing a class of bug (NullPointerExceptions) even without the rest of Monadkind.
> ?. is a special-case operation on nullables, if you want to use it on any of the other things that flatMap works on (e.g., lists), you need a different operation, so you can't build generic algorithms.
Being able to use generic algorithms like sort() on Maybes-as-collections-of-arity-[0,1], while very cute, isn't actually that useful in real code. Particularly real C# or Java code.
Don't get me wrong, I've written code in Scala, and I love the generality of Maybe and related collection types, even though I have hit some interesting issues where I've needed to call .toSeq on my Maybe in order to get the right thing to happen, because they're not quite equivalent. But being pragmatic, and given that C# (and Java) don't have proper Monadic Maybe, and are unlikely to ever get them, I'd quite like the ?. and ?? operators, please.
[1] http://www.fastcompany.com/28121/they-write-right-stuff/
I think the point about the mathematics being too difficult for a "rank and file" programmer is probably a little off base. It isn't so much that the concepts are difficult as the fact that it seems prohibitively time consuming for relatively little gain that would put most people (especially those managing a project) off using formal specification / verification to build their software.
In most cases besides safety critical systems, it is acceptable to ship a product in 1/10th of the time, knowing that there is chance that there are imperfections.
Additionally, having used the Z language mentioned in the article, and taken some classes in university on formal methods, the thing which put me off the most was the (necessary) verbosity of the specification languages that are used for these type of things. I never wrote something that wasn't incredibly trivial, because it would have taken too long.
For me, the most useful thing about learning some of this is that while I never, in practice, do fully formal proofs, I make informal arguments for correctness as I write and I think about what it would take to formalize them - what is the invariant, preconditions etc. here? For the tricky bits, I will write out an informal argument for correctness and include it as a comment.
According to the article, Praxis is not using formal proofs exclusively, or even predominately, and is using Z mainly for the precise expression of ideas, while keeping them free of unnecessary implementation detail (in other words, for abstraction.)
http://www.amazon.com/Error-Free-Software-Know-How-Correctne...
Title/byline: "A small British firm shows that software bugs aren't inevitable (2005)"
Article: "Praxis doesn't claim it can make bug-free software, says Amey, now the company's chief technical officer. But he says the methodology pays off. Bugs are notoriously hard to count, and estimates of how common they are vary hugely. With an average of less than one error in every 10 000 lines of delivered code, however, Praxis claims a bug rate that is at least 50--and possibly as much as 1000--times better than the industry standard."
It's impressive, and I'd like to see more formal verification in software especially for security-critical components. But the title is factually incorrect.
""" Only after Praxis's engineers are sure that they have logically correct specifications written in Z do they start turning the statements into actual computer code. The programming language they used in this case, called Spark, was also selected for its precision. Spark, based on Ada, a programming language created in the 1970s and backed by the U.S. Department of Defense, was designed by Praxis to eliminate all expressions, functions, and notations that can make a program behave unpredictably. """
Is not only a problem that our industry lack discipline, is that almost everyone is so resistant to use better tools.
When some insist to use C++/JavaScript/PHP/MySql/Mongo/etc (tools with bad design/complexity/bug-prone/etc flaws) with the excuse that is possible to use them "well" if only we are more "disciplined" and "pay attention"?
When bad tools are bad, discipline is not the answer. Is fix the tool, or get rid of them.
Why developers understand that if a end-user have a high-error rate in one program is a problem with the program but when that happend with a language/tool for developers... not think the same???
How much do formal methods really buy us it terms of quality? What's the defect rate if you use language X vs language Y? Is it better to spend lots of time gathering requirements and then produce something that exactly matches the requirements or is it better to iterate as quickly as possible and gather requirements as you go? What's the impact of the team as compared to the methodology?
I suspect the answers to these questions are really murky and its not clear whether there is a single methodology that produces the best quality for the money invested.
The problem is, having spent seven years on a PSP/TSP team, that it greatly slows the development process so it's really only useful for those few types of projects where the cost of quality is worth it. For the vast majority of software, I'd say that it's better to accept a small number of minor defects in order to ship faster.
If everyone did what Praxis does software would work more reliably, but there would be far fewer programmers and - crucially - far fewer projects of all kinds.
We have the software industry we have because businesses don't want to pay for a better industry. It's the classic "worse is better" dilemma.
If software were rigorous, the initial cost of many projects would make them look prohibitively expensive. You can try to argue that total costs, including fixes and maintenance, are much lower, but not many managers are going to pay n times more for a project up front in the hope the cost will be n times less over its lifetime - even if there's a serious risk of paying millions or billions and literally getting nothing of use, as regularly happens on very big contracts.
Eventually quality would get cheaper. But for now it's as if the entire field is drowning in technical debt, buried under me-too frameworks and languages that do very little to genuinely improve productivity or reliability, supported by "Take the money, promise everything, and hope for the best" commercial attitudes.
Unfortunately you'd have to wipe out so many languages, techniques, ideas, systems, practices, and management attitudes, and put so many people out of work - or force them into retraining - that the kind of bug rates Praxis produce are never going to be possible across the industry as a whole.
"The key weapon is abstraction," he says. "If you can build abstractions well enough, you should be able to break things down into bits you can handle." That maxim guides every other discipline in engineering, not least the design of computer hardware. Why not apply it to software, too?
One the whole, we do. But sometimes abstractions leak [1]. Sometimes you get impedance mismatches when you try to layer them. Sometimes the abstraction isn't what you think it is or want it to be.
An example of the last point is alluded to in a comment by efaref about a binary search algorithm that turned-out to be broken because it assumed that an integer type in the implementation language behaved the same way as integers in mathematics, but it didn't because it didn't allow arbitrary-size values. The abstraction provided by the integer type was faulty.