8 ms·

> Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). That's the thing though, the "soc

by erokar 9y ago

> Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). That's the thing though, the "social problems" are the important problems. I think it's a given you should use strong type systems in safety critical software — Haskell, for instance. But look at the quote from Dr Nancy Leveson: I've been doing this for thirty-six years. I've read hundreds of accident reports and many of them have software in them. And every someone (sic) that software was related, it was a requirements problem. It was not a coding problem. So that's the first really important thing. Everybody's working on coding and testing and they're not working on the requirements, which is the problem. Lack of strong typing does not seem to be the issue. Lacking domain understanding/logical errors is the problem.

Silhouette 9y ago
I've been doing this for thirty-six years. I've read hundreds of accident reports and many of them have software in them. And every someone (sic) that software was related, it was a requirements problem. It was not a coding problem. That part put me off, because while awareness of problems with the requirements themselves is much lower than IMHO it could beneficially be, the casual dismissal of coding errors as another cause of failures makes me question where this "expert" has any idea what they're talking about at all, thirty-six years or not. There is a reason that Tony Hoare called inventing null references his billion-dollar mistake! Edit: Having watched the original presentation by that speaker, in context and without any emphasis or commentary added by anyone else, the above criticism is unfair and I apologise for it. I think the subsequent discussions of it here may be putting more weight on that line than is justified, though, as you still have to have enough other mechanisms in place to avoid the coding errors making it into production before Dr Leveson's comments would apply.
- coldtea 9y ago
  >the casual dismissal of coding errors as another cause of failures makes me question where this "expert" has any idea what they're talking about at all, thirty-six years or not They don't dismiss them casually. She dismisses them because of actual experience on not having seen those matter much for 36 years, in all kinds of scenarios where she was explicitly looking for such things. >There is a reason that Tony Hoare called inventing null references his billion-dollar mistake! Which is neither here nor there, as in the domain we're she works, they don't allow those mistakes to go through to begin with.
- fsloth 9y ago
  "casual dismissal of coding errors as another cause of failures" It'd not casual dismissal. What she says that despite how good a job developers do, not understanding the basic domain where the software operates will lead to a failure in production environment. Which, really, makes sense. Requirements drive the test envelope. Generally, people try to test the product they are releasing - but if they do not foresee a testable scenario then that is not tested. The best way to let bugs slip through is not to test against them.
solatic 9y ago
There is the school of thought though that type-driven development, by forcing domain understanding to be expressed in terms of types, helps to create common domain understanding among the different stakeholders.
blub 9y ago
I'm curious how OP would prevent the Therac incident through type systems... Key quote: "Previous models had hardware interlocks in place to prevent this, but Therac-25 had removed them, depending instead on software interlocks for safety." Or even better how type systems could work around data integrity errors in RAM without ECC.
- kazinator 9y ago
  Maybe I'm recalling things wrong (the incident is very old and I last read the details before some HN-ers here were born), but at the heart of the Therac-25 issue was flaky code, written in a language without any type enforcement (assembly language). What's worse, the code was juggling concurrent events with interrupts and whatnot and was laden with race conditions (probably a phrase not even in the developer's vocabulary).
  - blub 9y ago
    Pages 42-end of Leveson's report explain the fixes put in place and the contributing causes. Software bugs are a contributing factor, but the report warns against focusing myopically on the bugs.
- SomeStupidPoint 9y ago
  > Or even better how type systems could work around data integrity errors in RAM without ECC. You realize that you can do ECC in software too, right? You just need the statistical bound on a double fault to be similar to that of the hardware case. Type systems can be used to do this by defining an interface for the data, letting you swap between normal datatypes and ECC ones seamlessly. (And in practice, you only need to define the base operators for your new type.) You can do this with ducktyping ECC versions of objects in say... Python. But the type system helps ensure that you've built the full set of components necessary and it properly links. You have to do this with ad hoc IDE tools in Python. Similarly.... > The defect was as follows: a one-byte counter in a testing routine frequently overflowed; if an operator provided manual input to the machine at the precise moment that this counter overflowed, the interlock would fail. That actually sounds like exactly the situation that a type system would be used to prevent -- partly because from a type theoretic perspective, that whole situation sounds like an obvious defect. Further, the result was because of an obscure combination of key strokes that went untested. The use of total functions (enforced by the type system) lets you verify (by computer) that no combination of input can transition to a bad state. So... Did you intentionally pick two cases where type systems are the obvious solution to the problem?
naasking 9y ago
> That's the thing though, the "social problems" are the important problems. And yet, we still seem bogged down with bugs and vulnerabilities caused by non-social problems. So use types to get rid of those problems, and then we can worry about the social problems. > Lack of strong typing does not seem to be the issue. Lacking domain understanding/logical errors is the problem. Types help with this too. Formalizing a property that is inconsistent, underspecified, or over-constrained is a natural part of designing a type to represent that property.
- Jtsummers 9y ago
  So formalizing things with type systems is great. In fact, I'm a huge proponent of it. The problem still remains, you may not have a sufficiently well developed requirement set to be able to specify things in your type system. I'll give an example: It's possible in Haskell (really many languages) to create a type SafeString which can be constructed from a standard String and does all the necessary escaping for the target (let's say it takes in a username and works to prevent sql injection attempts, or removes HTML tags, or whatever might be appropriate). And for all practical purposes it behaves exactly like a string otherwise. Any time you want to make a SQL query or generate some HTML you know that you can use a SafeString and it'll (barring errors in implementation) work without causing you either security risks or producing incorrect outputs. That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this. The type system itself doesn't tell you that your types are underspecified. It needs to come from the requirements analysis (in this case, requirements as viewed through a security-oriented perspective). But type systems allow you to encode that specification once it's been made.
  - naasking 9y ago
    > That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this. The type system itself doesn't tell you that your types are underspecified. Indeed type checking alone won't tell you that, but my point was more that type-driven design has a much better chance at revealing such underspecified requirements. If you resist the urge to be lazy by assuming that your domain types map perfectly to built-in types, like String or Int32, and instead assume that your domain needs its own types, you centralize the validation logic to create domain types, which can then be easily audited and tested. So you should create a distinct SafeString or SqlQuery type as a natural part of modelling your domain, even if the semantics of String appear sufficient.

by erokar 9y ago

Silhouette 9y ago

I've been doing this for thirty-six years. I've read hundreds of accident reports and many of them have software in them. And every someone (sic) that software was related, it was a requirements problem. It was not a coding problem. That part put me off, because while awareness of problems with the requirements themselves is much lower than IMHO it could beneficially be, the casual dismissal of coding errors as another cause of failures makes me question where this "expert" has any idea what they're talking about at all, thirty-six years or not. There is a reason that Tony Hoare called inventing null references his billion-dollar mistake! Edit: Having watched the original presentation by that speaker, in context and without any emphasis or commentary added by anyone else, the above criticism is unfair and I apologise for it. I think the subsequent discussions of it here may be putting more weight on that line than is justified, though, as you still have to have enough other mechanisms in place to avoid the coding errors making it into production before Dr Leveson's comments would apply.

coldtea 9y ago
>the casual dismissal of coding errors as another cause of failures makes me question where this "expert" has any idea what they're talking about at all, thirty-six years or not They don't dismiss them casually. She dismisses them because of actual experience on not having seen those matter much for 36 years, in all kinds of scenarios where she was explicitly looking for such things. >There is a reason that Tony Hoare called inventing null references his billion-dollar mistake! Which is neither here nor there, as in the domain we're she works, they don't allow those mistakes to go through to begin with.
fsloth 9y ago
"casual dismissal of coding errors as another cause of failures" It'd not casual dismissal. What she says that despite how good a job developers do, not understanding the basic domain where the software operates will lead to a failure in production environment. Which, really, makes sense. Requirements drive the test envelope. Generally, people try to test the product they are releasing - but if they do not foresee a testable scenario then that is not tested. The best way to let bugs slip through is not to test against them.

solatic 9y ago

There is the school of thought though that type-driven development, by forcing domain understanding to be expressed in terms of types, helps to create common domain understanding among the different stakeholders.

blub 9y ago

I'm curious how OP would prevent the Therac incident through type systems... Key quote: "Previous models had hardware interlocks in place to prevent this, but Therac-25 had removed them, depending instead on software interlocks for safety." Or even better how type systems could work around data integrity errors in RAM without ECC.

kazinator 9y ago
Maybe I'm recalling things wrong (the incident is very old and I last read the details before some HN-ers here were born), but at the heart of the Therac-25 issue was flaky code, written in a language without any type enforcement (assembly language). What's worse, the code was juggling concurrent events with interrupts and whatnot and was laden with race conditions (probably a phrase not even in the developer's vocabulary).
- blub 9y ago
  Pages 42-end of Leveson's report explain the fixes put in place and the contributing causes. Software bugs are a contributing factor, but the report warns against focusing myopically on the bugs.
SomeStupidPoint 9y ago
> Or even better how type systems could work around data integrity errors in RAM without ECC. You realize that you can do ECC in software too, right? You just need the statistical bound on a double fault to be similar to that of the hardware case. Type systems can be used to do this by defining an interface for the data, letting you swap between normal datatypes and ECC ones seamlessly. (And in practice, you only need to define the base operators for your new type.) You can do this with ducktyping ECC versions of objects in say... Python. But the type system helps ensure that you've built the full set of components necessary and it properly links. You have to do this with ad hoc IDE tools in Python. Similarly.... > The defect was as follows: a one-byte counter in a testing routine frequently overflowed; if an operator provided manual input to the machine at the precise moment that this counter overflowed, the interlock would fail. That actually sounds like exactly the situation that a type system would be used to prevent -- partly because from a type theoretic perspective, that whole situation sounds like an obvious defect. Further, the result was because of an obscure combination of key strokes that went untested. The use of total functions (enforced by the type system) lets you verify (by computer) that no combination of input can transition to a bad state. So... Did you intentionally pick two cases where type systems are the obvious solution to the problem?

naasking 9y ago

> That's the thing though, the "social problems" are the important problems. And yet, we still seem bogged down with bugs and vulnerabilities caused by non-social problems. So use types to get rid of those problems, and then we can worry about the social problems. > Lack of strong typing does not seem to be the issue. Lacking domain understanding/logical errors is the problem. Types help with this too. Formalizing a property that is inconsistent, underspecified, or over-constrained is a natural part of designing a type to represent that property.

Jtsummers 9y ago
So formalizing things with type systems is great. In fact, I'm a huge proponent of it. The problem still remains, you may not have a sufficiently well developed requirement set to be able to specify things in your type system. I'll give an example: It's possible in Haskell (really many languages) to create a type SafeString which can be constructed from a standard String and does all the necessary escaping for the target (let's say it takes in a username and works to prevent sql injection attempts, or removes HTML tags, or whatever might be appropriate). And for all practical purposes it behaves exactly like a string otherwise. Any time you want to make a SQL query or generate some HTML you know that you can use a SafeString and it'll (barring errors in implementation) work without causing you either security risks or producing incorrect outputs. That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this. The type system itself doesn't tell you that your types are underspecified. It needs to come from the requirements analysis (in this case, requirements as viewed through a security-oriented perspective). But type systems allow you to encode that specification once it's been made.
- naasking 9y ago
  > That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this. The type system itself doesn't tell you that your types are underspecified. Indeed type checking alone won't tell you that, but my point was more that type-driven design has a much better chance at revealing such underspecified requirements. If you resist the urge to be lazy by assuming that your domain types map perfectly to built-in types, like String or Int32, and instead assume that your domain needs its own types, you centralize the validation logic to create domain types, which can then be easily audited and tested. So you should create a distinct SafeString or SqlQuery type as a natural part of modelling your domain, even if the semantics of String appear sufficient.