3 ms·

That's true for all programming languages. That's literally how all bugs get created. Are you claiming that there exists some language where bugs cannot happen

That's true for all programming languages. That's literally how all bugs get created. Are you claiming that there exists some language where bugs cannot happen because it is "type safe"?

catnaroek 10y ago
> That's true for all programming languages. I'm pretty sure that when I define abstract types in ML, I can often arrange things so that they mean what I want them to mean. For example, I can define set and heap types that are impossible to use in any other way than as sets or heaps. Of course, I still have to manually prove that my implementation is correct, but the language guarantees that, if my implementation is correct, it's impossible to misuse. The problem with Go is that the type system is too dumb to actually enforce such things, so the names of your types are nothing but declarations of good intentions. So you might as well use a dynamically typed language, since you have nothing to lose but the verbosity. > Are you claiming that there exists some language where bugs cannot happen because it is "type safe"? No, I didn't say that.
- adamlett 10y ago
  The problem with Go is that the type system is too dumb to actually enforce such things First of all, if there is one problem that is the problem with Go, I doubt that many Go programmers would agree that what you describe is it. Secondly, what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. A type is nothing more than a statement about an interesting property of a program which can be checked by a computer. Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Whether or not the program halts is the most famous. Some type systems are obviously more capable than others, but it's a spectrum. There is no divide between type safe and type unsafe.
  - catnaroek 10y ago
    > what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. Not really. In a language with abstract data types, such as ML, an ordered set type only has actual ordered sets as its values. Languages without abstract types (not the same thing as abstract classes) are hobbled. > Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Who says everything has to be machine-verified? Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. You'd be surprised how much can be machine-verified if you arrange things properly. > Whether or not the program halts is the most famous. The lack of a general procedure for determining termination doesn't prevent you from proving it manually. For instance, a recursive function defined by structural induction on its argument is guaranteed to terminate. This covers most of the code I want to write in practice.
    - adamlett 10y ago
      Not really. […] You seem to have missed the last part where I wrote "for appropriate values of such things". I didn't claim that all type systems have the exact limitations of Go, but merely that all type systems have limitations. Who says everything has to be machine-verified? I don't know. Certainly not I. But I'm sure you agree that it would be nice if more things were. Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. Yeah, unfortunately there are some things that neither machines nor humans are great at checking. But I agree of course. My point is still simply that you are drawing the line between type safe and not type safe arbitrarily. There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust.
      - catnaroek 10y ago
        > There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust. It's not about power. It's about fulfilling your promises. For instance, neither ML nor Go promises to prevent you from trying to use files after closing them. But C++ and Rust do, and it turns out only Rust actually fulfills this promise. Go is actually type safe for single-threaded use. However, it doesn't deliver on its promise of safe concurrency. If you send an object to another goroutine, say, via a channel, nothing prevents you from mutating the same object from both the sender and the receiver, without any sort of concurrency control. Of course, a corollary of all the above is that type safety buys you different things in different languages.

That's true for all programming languages. That's literally how all bugs get created. Are you claiming that there exists some language where bugs cannot happen because it is "type safe"?

catnaroek 10y ago

> That's true for all programming languages. I'm pretty sure that when I define abstract types in ML, I can often arrange things so that they mean what I want them to mean. For example, I can define set and heap types that are impossible to use in any other way than as sets or heaps. Of course, I still have to manually prove that my implementation is correct, but the language guarantees that, if my implementation is correct, it's impossible to misuse. The problem with Go is that the type system is too dumb to actually enforce such things, so the names of your types are nothing but declarations of good intentions. So you might as well use a dynamically typed language, since you have nothing to lose but the verbosity. > Are you claiming that there exists some language where bugs cannot happen because it is "type safe"? No, I didn't say that.

adamlett 10y ago
The problem with Go is that the type system is too dumb to actually enforce such things First of all, if there is one problem that is the problem with Go, I doubt that many Go programmers would agree that what you describe is it. Secondly, what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. A type is nothing more than a statement about an interesting property of a program which can be checked by a computer. Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Whether or not the program halts is the most famous. Some type systems are obviously more capable than others, but it's a spectrum. There is no divide between type safe and type unsafe.
- catnaroek 10y ago
  > what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. Not really. In a language with abstract data types, such as ML, an ordered set type only has actual ordered sets as its values. Languages without abstract types (not the same thing as abstract classes) are hobbled. > Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Who says everything has to be machine-verified? Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. You'd be surprised how much can be machine-verified if you arrange things properly. > Whether or not the program halts is the most famous. The lack of a general procedure for determining termination doesn't prevent you from proving it manually. For instance, a recursive function defined by structural induction on its argument is guaranteed to terminate. This covers most of the code I want to write in practice.
  - adamlett 10y ago
    Not really. […] You seem to have missed the last part where I wrote "for appropriate values of such things". I didn't claim that all type systems have the exact limitations of Go, but merely that all type systems have limitations. Who says everything has to be machine-verified? I don't know. Certainly not I. But I'm sure you agree that it would be nice if more things were. Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. Yeah, unfortunately there are some things that neither machines nor humans are great at checking. But I agree of course. My point is still simply that you are drawing the line between type safe and not type safe arbitrarily. There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust.
    - catnaroek 10y ago
      > There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust. It's not about power. It's about fulfilling your promises. For instance, neither ML nor Go promises to prevent you from trying to use files after closing them. But C++ and Rust do, and it turns out only Rust actually fulfills this promise. Go is actually type safe for single-threaded use. However, it doesn't deliver on its promise of safe concurrency. If you send an object to another goroutine, say, via a channel, nothing prevents you from mutating the same object from both the sender and the receiver, without any sort of concurrency control. Of course, a corollary of all the above is that type safety buys you different things in different languages.