5 ms·

Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Relatively

Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Relatively little behavior can be encoded in inexpressive type systems, so there's a lot of room for bugs that have nothing to do with types. A lot more behavior (e.g. the sorts of invariants mentioned in agentultra's top level comment) can be encoded in a more expressive type system, but you then have the challenge of encoding it /correctly/. A lot of that kind of thinking is the same as the kind of thinking you'd have to do writing in a dynamic language, but you get more assurances when your type system gives you feedback about whether you're thinking about the problem right. For my money, I work in a primarily dynamic language and I already have a set of practices that usually prevent relatively simple type mismatches so I very rarely see bugs slip into production that involve type mismatches that would be caught by a Go-level type system, and just that level of type information would add a lot of overhead to my code. But if I were already using types, a more expressive system could probably catch a lot of invariance issues. So I feel like the sweet spot graph is more bimodal for me: the initial cost of switching to a basic static type system wouldn't buy me a lot in terms of effort-to-caught-bugs-ratio, but there's a kind of longer term payout that might make it worth it as the type system becomes more expressive.

pdonis 9y ago
> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that doesn't do what the user actually wants it to do. Static typing doesn't catch that.
- avg_programmer 9y ago
  The article was not trying to discuss how to make programmers smarter. No language is going to help with that so there is no point in talking about it. As far as the scope of the article is concerned, it's fair to say that statically verified code equals bug-free code.
- icebraining 9y ago
  Or as Knuth pithily put it, "Beware of bugs in the above code; I have only proved it correct, not tried it."
- naasking 9y ago
  > It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that doesn't do what the user actually wants it to do. Static typing doesn't catch that. It's also possible to grab a knife with your hand on the blade edge and cut yourself, but that doesn't diminish safety the value of knife handles.
- zbobet2012 9y ago
  It depends on your type system. In new languages like Idris or F* you can encode in the type the correctness of an algorithm and it will not compile if the compiler can not prove that correctness. For example I can prove my my string reverse works in Idris (https://www.stackbuilders.com/news/reverse-reverse-theorem-proving-with-idris https://www.stackbuilders.com/news/reverse-reverse-theorem-p...). Or I could prove that my function squares all elements in a list. Etc. Now a big part of the problem is expressing with sufficient accuracy what the properties of the algorithm you want to prove are. For example for string reverse I may want to show more than that `reverse (reverse s) = s`. Since after all if reverse does nothing that would still be true. I would probably want to express that the first and last chars swap when I just call reverse xs.
  - Merovius 9y ago
    > For example I can prove my my string reverse works in Idris (https://www.stackbuilders.com/news/reverse-reverse-theorem-p... https://www.stackbuilders.com/news/reverse-reverse-theorem-p...). This article basically demonstrates GP point, though. It proves that `reverse` is self-inverse, but there are lots and lots of functions that are self-inverse (for example, `x -> x` is self-inverse. As would be the function that swaps any odd-index element with the one following it). The claim was a difficulty of how to encode the actual correctness into your type-system. That this article doesn't actually encode correctness of reverse, seems like pretty good for that difficulty.
    - zbobet2012 9y ago
      This is precisely what I said in the next paragraph and even mentioned away to correctly encode that "correctness". Where a _correct_ implementation of reverse has the property `strHead' s = strTail' (reverse s)` recursively. It's important to understand that type systems can encode correctness to the level you can specify it. So the program is therefore bug-free to the accuracy of your requirements on it. Most people do not work with type systems which can do this and are unfamiliar with formal verification. The author presents directly (and argues through out) that there is a correlation not that bug free and static analysis are the same thing.
- Merovius 9y ago
  > The author of the article implicitly equates "statically verified code" with "bug-free code". Not at all. First, the statements as put here are discrete (boolean even) while I present both "statically verified code" and "bug-freedom" as living on a continuum. Secondly, I don't equate them. If anything, I assume a monotonic, positive relationship between them (strictly speaking not even that. I make pretty clear that the curves could also have whatever shape. But I yield that I am very suggestive in this because I do strongly believe it to be the case). In fact, one of the main points of the argument is that the two are not equal - otherwise, the blue curves I drew would all be straight lines from (0,0) to (1,1). And lastly, none of this is done implicitly. I mention all of this pretty explicitly :)
hellofunk 9y ago
> I already have a set of practices that usually prevent relatively simple type mismatches Care to share those practices? I also primarily work (this year, at least) in dynamically typed languages.
- catpolice 9y ago
  I think it depends on language and context a lot so I can only give some vauge advice. A lot of the idea is to write code that only does the one thing you know you need it to do, does it very simply and fails very obviously when it's not used correctly. In some cases your instinct is to make things as generic as possible at the first pass. Preemptive abstraction pays off more in statically typed languages, in my experience, because it saves you the time of refactoring a type system in place if you turn out to need flexibility later. But in dynamic languages it can introduce complexity that hides bugs. Simple type-level errors come up the most when you have types that are easily conflated. That tends to happen when you have functions that accept more than one type of thing or output more than one type of thing - avoid that. Avoid polymorphism and OOP patterns that set up a complicated type hierarchy or override methods - you don't want any instance where you end up with something that looks a lot like one type of thing but isn't. Type hierarchies can often be factored out into behaviors provided by modules that supply functions that operate on plain data structures. For variables and parameters, stick to really simple types to whatever degree it's possible, e.g. language primitives, plain old data-container objects and "maybe" types (e.g. things that could be a primitive or null) when absolutely necessary (and check them whenever you might have one). Use union types extremely sparingly. Assignment/creation bottlenecks are useful: try to have only one source for objects of a certain type that always constructs them the same way (so you don't end up with missing fields). A lot of programmers coming from a language with a stronger type system (especially when transitioning from OOP languages to functional or hybrid languages) tend to be nervous about writing functions without a guarantee about what kind of inputs they'll see, so they try to compensate for the lack of type safety by building functions that can cope with whatever is thrown at them. The idea is that this makes the function more robust but ironically, this tends to make bugs a lot harder to track down. In my experience it's better to write functions with specific expectations about their input that fast-fail if those aren't met, instead of trying to recover in some way - garbage-in-exceptions-out is better than garbage-in-garbage-out. If you send the wrong kind of thing to a function, you want it to throw an error then and there, and you'll likely catch it the first time you test that code. A lot of the idea of this kind of advice is to shift the work that would be done by the compiler's type system to the very first pass of testing - if your program is basically a bunch of functions that only take one sort of thing in each argument slot, only emit one sort of thing as a result and fail fast when those expectations are violated, you'll typically see runtime type errors the first time those functions get executed, which is a lot like seeing them at compile time.
32days8kd 9y ago
I had a related reaction, which is that the problems you're mentioning can become more complex when using libraries outside the standard library with static languages. E.g., my experience is that poor library design can sometimes be exacerbated in statically typed languages if the type logic is poor and doesn't match the problem domain. Dynamic languages sometimes inadvertently "correct" for this by smoothing over these sorts of issues. I prefer static languages (or at least optionally typed ones) but there can be big downsides of the sort you're mentioning, that are exacerbated by third-party libraries.
catnaroek 9y ago
> but you get more assurances when your type system gives you feedback about whether you're thinking about the problem right. It really isn't as much about languages as it is about the people who use them. The key ability is to prove things about programs. Powerful type systems, especially those that have type inference, merely relieve the programmer from some of the most boring parts of the job. Sometimes.
yawaramin 9y ago
> ... and just that level of type information would add a lot of overhead to my code. Can you give an example of this overhead?

pdonis 9y ago

> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that doesn't do what the user actually wants it to do. Static typing doesn't catch that.

avg_programmer 9y ago
The article was not trying to discuss how to make programmers smarter. No language is going to help with that so there is no point in talking about it. As far as the scope of the article is concerned, it's fair to say that statically verified code equals bug-free code.
icebraining 9y ago
Or as Knuth pithily put it, "Beware of bugs in the above code; I have only proved it correct, not tried it."
naasking 9y ago
> It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that doesn't do what the user actually wants it to do. Static typing doesn't catch that. It's also possible to grab a knife with your hand on the blade edge and cut yourself, but that doesn't diminish safety the value of knife handles.
zbobet2012 9y ago
It depends on your type system. In new languages like Idris or F* you can encode in the type the correctness of an algorithm and it will not compile if the compiler can not prove that correctness. For example I can prove my my string reverse works in Idris (https://www.stackbuilders.com/news/reverse-reverse-theorem-proving-with-idris https://www.stackbuilders.com/news/reverse-reverse-theorem-p...). Or I could prove that my function squares all elements in a list. Etc. Now a big part of the problem is expressing with sufficient accuracy what the properties of the algorithm you want to prove are. For example for string reverse I may want to show more than that `reverse (reverse s) = s`. Since after all if reverse does nothing that would still be true. I would probably want to express that the first and last chars swap when I just call reverse xs.
- Merovius 9y ago
  > For example I can prove my my string reverse works in Idris (https://www.stackbuilders.com/news/reverse-reverse-theorem-p... https://www.stackbuilders.com/news/reverse-reverse-theorem-p...). This article basically demonstrates GP point, though. It proves that `reverse` is self-inverse, but there are lots and lots of functions that are self-inverse (for example, `x -> x` is self-inverse. As would be the function that swaps any odd-index element with the one following it). The claim was a difficulty of how to encode the actual correctness into your type-system. That this article doesn't actually encode correctness of reverse, seems like pretty good for that difficulty.
  - zbobet2012 9y ago
    This is precisely what I said in the next paragraph and even mentioned away to correctly encode that "correctness". Where a _correct_ implementation of reverse has the property `strHead' s = strTail' (reverse s)` recursively. It's important to understand that type systems can encode correctness to the level you can specify it. So the program is therefore bug-free to the accuracy of your requirements on it. Most people do not work with type systems which can do this and are unfamiliar with formal verification. The author presents directly (and argues through out) that there is a correlation not that bug free and static analysis are the same thing.
Merovius 9y ago
> The author of the article implicitly equates "statically verified code" with "bug-free code". Not at all. First, the statements as put here are discrete (boolean even) while I present both "statically verified code" and "bug-freedom" as living on a continuum. Secondly, I don't equate them. If anything, I assume a monotonic, positive relationship between them (strictly speaking not even that. I make pretty clear that the curves could also have whatever shape. But I yield that I am very suggestive in this because I do strongly believe it to be the case). In fact, one of the main points of the argument is that the two are not equal - otherwise, the blue curves I drew would all be straight lines from (0,0) to (1,1). And lastly, none of this is done implicitly. I mention all of this pretty explicitly :)

hellofunk 9y ago

> I already have a set of practices that usually prevent relatively simple type mismatches Care to share those practices? I also primarily work (this year, at least) in dynamically typed languages.

catpolice 9y ago
I think it depends on language and context a lot so I can only give some vauge advice. A lot of the idea is to write code that only does the one thing you know you need it to do, does it very simply and fails very obviously when it's not used correctly. In some cases your instinct is to make things as generic as possible at the first pass. Preemptive abstraction pays off more in statically typed languages, in my experience, because it saves you the time of refactoring a type system in place if you turn out to need flexibility later. But in dynamic languages it can introduce complexity that hides bugs. Simple type-level errors come up the most when you have types that are easily conflated. That tends to happen when you have functions that accept more than one type of thing or output more than one type of thing - avoid that. Avoid polymorphism and OOP patterns that set up a complicated type hierarchy or override methods - you don't want any instance where you end up with something that looks a lot like one type of thing but isn't. Type hierarchies can often be factored out into behaviors provided by modules that supply functions that operate on plain data structures. For variables and parameters, stick to really simple types to whatever degree it's possible, e.g. language primitives, plain old data-container objects and "maybe" types (e.g. things that could be a primitive or null) when absolutely necessary (and check them whenever you might have one). Use union types extremely sparingly. Assignment/creation bottlenecks are useful: try to have only one source for objects of a certain type that always constructs them the same way (so you don't end up with missing fields). A lot of programmers coming from a language with a stronger type system (especially when transitioning from OOP languages to functional or hybrid languages) tend to be nervous about writing functions without a guarantee about what kind of inputs they'll see, so they try to compensate for the lack of type safety by building functions that can cope with whatever is thrown at them. The idea is that this makes the function more robust but ironically, this tends to make bugs a lot harder to track down. In my experience it's better to write functions with specific expectations about their input that fast-fail if those aren't met, instead of trying to recover in some way - garbage-in-exceptions-out is better than garbage-in-garbage-out. If you send the wrong kind of thing to a function, you want it to throw an error then and there, and you'll likely catch it the first time you test that code. A lot of the idea of this kind of advice is to shift the work that would be done by the compiler's type system to the very first pass of testing - if your program is basically a bunch of functions that only take one sort of thing in each argument slot, only emit one sort of thing as a result and fail fast when those expectations are violated, you'll typically see runtime type errors the first time those functions get executed, which is a lot like seeing them at compile time.

32days8kd 9y ago

I had a related reaction, which is that the problems you're mentioning can become more complex when using libraries outside the standard library with static languages. E.g., my experience is that poor library design can sometimes be exacerbated in statically typed languages if the type logic is poor and doesn't match the problem domain. Dynamic languages sometimes inadvertently "correct" for this by smoothing over these sorts of issues. I prefer static languages (or at least optionally typed ones) but there can be big downsides of the sort you're mentioning, that are exacerbated by third-party libraries.

catnaroek 9y ago

> but you get more assurances when your type system gives you feedback about whether you're thinking about the problem right. It really isn't as much about languages as it is about the people who use them. The key ability is to prove things about programs. Powerful type systems, especially those that have type inference, merely relieve the programmer from some of the most boring parts of the job. Sometimes.

yawaramin 9y ago

> ... and just that level of type information would add a lot of overhead to my code. Can you give an example of this overhead?