7 ms·

Curiously, in the list of possible future tools for more reliability type systems are absent. Looking at the authors bio: "I love solving tough problems with P

• 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.
• agumonkey 9y ago
  That's a social issue, people with diverse point of view, even if myopic will talk and create together because they can share and communicate about the issue at hand. Uncle Bob and others don't see what's good in having a bit of logic prover to look at a codebase.. well too bad. 10$ they will in time realize it's pretty pretty and pretty useful.
• bjpbakker 9y ago
  > I don't understand people arguing against type systems on principle I believe these are the people who relate type systems to languages like C++ and Java, and dismiss type systems as a possible solutions because they've only seen the poor ones. Back when I wrote a lot of Java code I mostly used TDD to write software that works. The type system didn't help that much. Robert "Uncle Bob" Martin dismisses type systems as "reducing the incidence of textual errors in a program" [0]. I doubt that Robert Martin is very familiar with very strong type systems such as in Idris, Coq, Haskell, etc. Many programmers (most I know actually) don't learn these languages as they aren't useful to get a better job, earn promotions, etc. [0] - http://blog.cleancoder.com/uncle-bob/2017/01/13/TypesAndTests.html http://blog.cleancoder.com/uncle-bob/2017/01/13/TypesAndTest...
  • blub 9y ago
    Well if one can't get a job programming Idris, Coq or Haskell and they're not used in OSS infrastructure software either, what's the point of learning them? Then they literally have zero direct effect on improving the safety of anything. One would be better off learning TLA+ and coding in C, or using Frama-C or Misra etc.
    • bjpbakker 9y ago
      > what's the point of learning them I personally enjoy learning new languages and I can always apply the concepts I learn in other languages that are used on the job. Not judging others who don't enjoy that, though. It's more surprising that there's no real incentive from companies to write better software. People seem to accept a whole lot of shit when it comes to their phones and computers, and are happy to pay for it.
• blub 9y ago
  Type systems are not enough. I'm not sure they're even a good starting point for safety critical software, but they might be good for e.g browsers. You're thinking at code level, people like Leveson, Knight and others are thinking at system level. The end goal is to have a safe system, not e.g avoid null pointer exceptions through optional types.
  • zoul 9y ago
    Optional types are a good example of how types make a system safer. Sure, they are a pretty low-level guarantee, but that still counts—and if you have an expressive type system, you can make much higher-level guarantees with types.
    • blub 9y ago
      I think they're great! I am pushing to use them in our C++ code base and they empirically do improve safety by transforming UB into a nice exception. But they won't prevent a programmer from using MD5 for RSA signature verification.
      • dkersten 9y ago
        But if all of these things are correctly typed, then it would be visually more likely for someone to notice that the algorithm doesn't return the type it says. Also, C++ static types are rather weak. Its optional types are useful, but its not like in SML where the compiler ensures that you handled all possible cases. A good type system can't catch all kinds of errors though.
  • gipp 9y ago
    I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. A full dependent type system is sufficient to statically prove that code meets a given specification. We're not just talking about ints and strings and optionals when we talk about type systems for correct software. See Curry-Howard correspondence.
    • 9y ago
• crdoconnor 9y ago
  >Personally, I don't understand people arguing against type systems on principle. Even Uncle Bob wasn't, I don't think. He just said that certain languages had type systems with a level of strictness that he considered too extreme. >Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems No, not all, only certain classes. With haskell, for example, that comes at the expense of development velocity and performance (or at least, the ability to reason about performance). >There has to be something I'm missing since there are so many people arguing against types, notably Bob Martin himself. I think the key part people miss in the "more strictness" argument is that stricter types lengthen development and if your biggest risk is errors in specification (the article makes assertion and in my domains, that's been my experience too), so you are risking a vast amount of wasted time spent on perfecting the wrong thing.
  • Silhouette 9y ago
    With haskell, for example, that comes at the expense of development velocity and performance (or at least, the ability to reason about performance). That seems a little unfair. The biggest challenge with reasoning about performance in Haskell is usually its non-strict semantics. That issue is only incidentally related to Haskell's type system being significantly more capable than those of many other programming languages.
  • tpush 9y ago
    > With haskell, for example, that comes at the expense of development velocity and performance (or at least, the ability to reason about performance). The (depending on perspective) weaker ability to reason about performance in Haskell stems from laziness, which itself has nothing to do with type systems. It's clashes with side-effects are solved _via_ the type system (The IO type). Regarding development velocity: _The developers_ are choosing how much time they spent on proving things to the type checker. Sure, writing a function that requires of its argument the type { n % 2 == 0 } or something is more labor intensive than just using Int and runtime panicking on invalid values. But you can choose do just that instead! There is no decree that on has to be as precise in their types as possible, no matter how much a given type system is able to express.
• coldtea 9y ago
  >Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). Yes, but they increase delivery time problems and developer time problems. In the end, the industry has decided getting something out cheaper and faster is worth more than getting it out correct code-wise but later or more expensively. Which might make perfect sense -- what's correct depends on business needs -- and some layers might be totally irrelevant (e.g. program design) as to that. >Personally, I don't understand people arguing against type systems on principle. Sure, they are type systems that suck (e.g. Java) or are otherwise very verbose and thus straining. But that doesn't have to be the case, it's not an intrinsic property of type systems. No, but not liking type systems might be an intrisic property of some programmers.
  • SomeStupidPoint 9y ago
    > No, but not liking type systems might be an intrisic property of some programmers I wish they'd stop writing shitty, ad hoc type systems into our production code, then.
  • magice 9y ago
    >Yes, but they increase delivery time problems and developer time problems. That's purely guesswork. Seriously! My observation is that as the size of the project grows, type system switches from hindrances to actually speed up development and save developer time. Ever try to grep weakly typed system for name definition? Yeah, you don't have that problem in strongly typed system. Lots of other reasoning are easier to do with types than without.
    • sheepmullet 9y ago
      > Ever try to grep weakly typed system for name definition? For what purpose?
      • coldtea 9y ago
        To understand a codebase?
• raverbashing 9y ago
  Division by zero is not a type problem, though it could be solved by creating a 'integer but not zero' type I'm sure if you spent the day creating types your software would be very reliable. It would also probably not do much "Relying on the power of type checking" is just wishful thinking that breaks down in the face of any moderately complex problem The problem of course is not the type system, the problem is people creating types that contain one int/string only when a boolean would suffice, or 10 types of almost similar containers because for some people "ifs are forbidden" Also reality likes to mess with well-oredered hierarchies
• tome 9y ago
  > Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). If you want a property to uphold, formulate it as a type. The compiler verifies. I'm a massive Haskell proponent and I'm calling you out because you're doing typed programming a massive injustice with this kind of overinflated claim. There is no known type system that can get anywhere near solving "all software reliability problems". Flexible type systems like Haskell's are really useful. Don't overpromise.
  • tpush 9y ago
    So where does it fall down? Excluding the social ones I mentioned.
    • tome 9y ago
      Can you prove the correctness of a sort function in the type system? I don't know any mainstream language where you can do that. You'd have to go to something like Agda, Idris, Coq or F* which are hardly practical languages (currently). Beyond that there's an entire universe of complexity that we have no idea how to prove (practically) in the type system. Haskell types encode simple properties. They're extremely useful properties in practice but they don't come anywhere near "everything" we would want to prove.
      • open_bear 9y ago
        What do you think about clojure.spec approach?
        • empthought 9y ago
          Those aren't proofs at all, and the docs even say so.
• humanrebar 9y ago
  > There has to be something I'm missing... Some of your replies have already touched on a few points, so I'll add a new one: type systems can be more than a lot of work, they can be wrong. You do allude to "formulating the type is too laborious", but it's more than that. For example, let's take the perennial question of object-relational mapping frameworks. "Object" isn't a great name for it because the real goal is usually a specific syntax (method calls) and type-safety features (make getID return an Integer, not a String). But there's a problem. "ID" is not the name of an attribute. It's a token in a SQL query. In the database, "ID" can be an Integer today, a nullable String tomorrow, and deleted next week. The type of the underlying data comes from the schema, not the application code. So there is inevitably a mismatch. Unless you understand there is some dynamism there and model the code that way. The same thing goes for strongly typed HTTP or SOAP clients. Also anything that parses input on the fly. There are absolutely places where the application can decide something has been validated and then apply that information to some data with a strong type, but there's a tradeoff there, too. You end up requiring that sort of validation-and-tagging in all sorts of places where it's irrelevant. Compare creating an XML DOM with using xpath, xquery, etc. You could create a giant graph of all the nodes in your XML document. Or you could just provide an expression that does pattern matching. There are places where either is handy, but the latter is almost always more flexible. Now, there are limits. Generally, well-typed data is easier for compilers to understand and optimized. That is, strongly typed data structures are important. But, honestly, most code isn't brand new data structures. Anyway, there's certainly balance to everything, but people need to keep in mind that type systems are a hammer like anything else. They can be misapplied harmfully, too. Caveat: It's possible to use generic programming and higher kinded types to work around many of these limitations, but I'm writing this blurb to people who are "application developers" or otherwise are big on object-oriented programming. If people are interested in how type systems can be more flexible, we can talk about that too. My point is that they overwhelmingly aren't used that way.
• shalabhc 9y ago
  > If you want a property to uphold, formulate it as a type. The compiler verifies. Consider two issues with this: 1. How do you verify that the property to uphold is indeed the same as formulated by the type? This is easier for simple types, but can get complicated real fast once you start getting into higher kinded types. Ideally you want the 'formulation' of the 'property to uphold' to be specified in the domain of the problem itself. 2. The compiler can only verify what it builds - but we don't build and deploy large systems all at once. We just build and deploy one subsystem - i.e. a single program at a time - into an already running system. So what about verification for coupling between different programs? (The Internet is dynamically typed). To solve #2, we might need some kind of run time negotiation and verification (and once you have that, perhaps it can that be used within each 'program' as well?).