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.
"1/10th of the time" implies that it takes 10 times longer to do the math than it does to stare at the screen with your head in your hands saying "oh god what have I done?" to yourself. I'd wager that's not the case.
It's a paradigm shift compared to the usual approach to programming, so I don't think it is for everybody, and realistically, it doesn't have to be.
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.)
I think an important thing that we're currently missing is some kind of quantitative assessment what influence various measures have on software quality. All we have are "best practices" that all sound like common sense, but without much data backing them.
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.
Actually all we have is faddy unrigorous hobbyisms, mediocre tools, and poor management.
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 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.
A referentially transparent, small function, has always been easy to write bug-free assuming the OS doesn't lose a page-table entry, a network interrupt isn't exploitable, and cosmic rays don't flip bits. The issue has never been that we can't write something that's correct.
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.
Also true. Still, purity (just part of referential transparency) should be highlighted as something that helps not just with the function you're writing , but also functions that need to call that function.
> With nicer syntax, nulls are equivalent to Maybe types.
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
I can also look up a User's spouse with either a Maybe or a NULL:
-- Maybe
getSpouse :: User -> Maybe User
-- Nullable
getSpouse :: User -> User
So far they're pretty much equivalent. However, what if I want to look up a spouse's DateOfBirth?
-- 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
These are no longer equivalent. In the Maybe case we can distinguish between three kinds of values:
- `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`).
Yeah, but you're comparing apples and oranges. The nullable case isn't preserving the information you want, because you haven't written the code to preserve it, while in your Maybe case, you have. The two examples you give aren't doing the same thing.
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
Likewise, the nullable case, modified to preserve it (in a language which actually has nulls this time):
> Your nullable example is better compared to this, which also discards the required information:
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
> Maybes are just pointers. There's nothing magic about them.
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.
> With nicer syntax, nulls are equivalent to Maybe types.
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.
> In a language that lacks maybes, but has nulls, what is the equivalent of the type Maybe (Maybe Int)?
int **
> 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.
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.
Even algorithms "proved" correct sometimes turn out to have bugs:
"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."
Interesting. The bug in the proof is in the assumption that ints contain any integer and addition operates the same in normal mathematics, when in fact they're the set of values in [INT_MIN, INT_MAX] and addition has overflow behaviour.
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.
I've been seriously considering doing a mini programming language where you can type-decorate numbers with exactly what behaviour you want and what their range is.
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).
Yes, Ada is a marvellous language. The exception is not named overflow, but constraint error. When used correctly, its typing system is very effective to avoid mistakes. The problem is that Ada types can become very annoying in bad code like the one produced by people with a very weak knowledge of the language. It is really too sad this language is almost not teached anymore in school.
Ha ha. I'd been reading HN on my phone, saw the parent comment, thought 'I should write a post about Ada', and when I got back to my computer, saw this...
Yes, ranges work. They (and ordinary integers) throw exceptions on overflow:
type NonoverflowingByte is integer range 0..255;
If you want modulus arithmetic, you specify it:
type OverflowingByte is mod 256;
Modulus types seem to be always unsigned and are always 0-based. Anyone know different?
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?)
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?
It's got a lot of historic warts. e.g. the OO system is a retrofit with invisible syntax: functions defined immediately after the type representing the object are methods, but you can't interleave them with other statements. It desperately needs an explicit `class...end` structure. The OO model is kinda weird, too, although once you've beaten your head against it it makes sense. Another wart is that you can only define an expression function in a module specification and not in a module body. Huh? Likewise, you can only define pre- or post-conditions on public data, so you can't have a module assert on its private state; you must export the state first.
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'.
Ada is up against C, C++, C# and Java. They all have larger everything - libraries, pool of programmers, support companies etc. Ada is doomed to spend its lifetime in the shadows. Pity, it is superior to all these languages, at least in my experience.
While not integer/number specific I like the idea of Guards in Elixir:
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"
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?
The exact size doesn't matter nearly as much as the fact that it has a bounded size. That changes the algebraic structure your proof operates on — and proofs on finite fields are often either general or at least give you results that explicitly depend on the size of the underlying set.
The exact size doesn't matter nearly as much as the fact that it has a bounded size. That changes the algebraic structure your proof operates on — and proofs on finite fields are often either general or at least give you results that explicitly depend on the size of the underlying set.
I suppose different people may answer your questions in different ways, depending on how they define words like "proof" and "correct". I would answer like this: the proof was correct, but it was solving the wrong problem (unbounded ints rather than bounded).
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.
There is a Google tech talk called "The Remote Agent Experiment: Debugging Code from 60 Million Miles Away" where the speaker describes how they did a proof that their code was deadlock free but it still ran into a deadlock. (I don't remember the details)
I've seen that example before, but I don't like it. It's an example of fixed-point overflow, but it wouldn't occur in practice.
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?
Maybe he probably proved the mathematical algorithm was correct. The problem is we have to implement algorithms using machines, which aren't perfect. They do a great job most of the time, but they exist in a physical environment which has restrictions and outside influences.
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.
For engineers, the last paragraph is the most pertinent:
"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.
If one were using formal methods in these circumstances, they should, in principle, reveal those leaks and impedance mismatches to you (or, more precisely, reveal to you any problems they cause in your specific design.) The existence of leaks and impedance matches in informal abstractions is an argument for formality, not against it.
I agree in principle, although in practice I am sceptical about the practicality of applying formal methods to large systems. The ratio of effort to reward just seems too large for most domains.
Can we change the title here? It's directly quoting the byline, but it contradicts the article.
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???
62 comments
[ 4.9 ms ] story [ 103 ms ] thread[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.
http://www.amazon.com/Error-Free-Software-Know-How-Correctne...
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.)
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.
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 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.
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:
I can also look up a User's spouse with either a Maybe or a NULL: So far they're pretty much equivalent. However, what if I want to look up a spouse's DateOfBirth? These are no longer equivalent. In the Maybe case we can distinguish between three kinds of values:- `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:
Likewise, the nullable case, modified to preserve it (in a language which actually has nulls this time): Maybes are just pointers. There's nothing magic about them.Exactly. Your version is just doing what `join` or `>>=` would do, which I mentioned at the end; ie.
> Maybes are just pointers. There's nothing magic about them.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.
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.
"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).
Don't remember how it handled overflow.
Yes, ranges work. They (and ordinary integers) throw exceptions on overflow:
If you want modulus arithmetic, you specify it: Modulus types seem to be always unsigned and are always 0-based. Anyone know different?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.
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.
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.
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?
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.
"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.
[1] https://en.wikipedia.org/wiki/Leaky_abstraction
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???