9 ms·

I think the comparison dwells on superficial similarities. Rust's type system is absolutely necessary to ensure a certain kind of safety under the requirements

by pron 7y ago

I think the comparison dwells on superficial similarities. Rust's type system is absolutely necessary to ensure a certain kind of safety under the requirements Rust adopted for itself in order to address certain domains (like no tracing GC), namely a guarantee of no undefined behavior, common in those domains. This safety (or something very close to it) exists in every so-called "managed" language anyway, be it Python, Java or Haskell, regardless of their type system, so the goal of the type system in Rust and in Haskell -- at least as far as safety goes -- is obviously very different. Moreover, such safety is not at all what is normally considered "correctness" in the field of software correctness; the term normally refers to functional correctness, i.e. that the program satisfies the specification, not that it doesn't have undefined behavior. On that front, there seems to be no evidence, nor even hints, that either Haskell or Rust do better, or worse, than other languages developed in recent decades. It's a myth, albeit one that's often repeated in some circles. That's not to say that type systems cannot be hugely valuable, and sometimes even necessary. For Rust, the type system is what ensures undefined-behavior-safety. In other languages it has many other advantages as well. Some type systems are even intended for correctness. But Rust's type system, and certainly Haskell's are not. Both are interesting though expressively "weak" type systems, of the kind that has not been found to be correlated with higher correctness. So focusing on that as the point of comparison completely misses the mark.

NOGDP 7y ago
> the term normally refers to functional correctness, i.e. that the program satisfies the specification, not that it doesn't have undefined behavior A program that has undefined behaviour is not correct, unless the spec has undefined behaviour (why would it?). > On that front, there seems to be no evidence, nor even hints, that either Haskell or Rust achieve better correctness (or the same correctness more cheaply). I don't know what you mean by evidence, but Haskell has a stronger and more expressive type system than say Java, it doesn't have null pointers, it has referential transparency, and simpler, safer concurrency and parallelism builtins. The fact that you can make more general assumptions about pieces of code which you don't necessarily fully understand makes writing safer and correct code easier. > But Rust's type system, and certainly Haskell's -- both interesting but very expressively "weak" type systems -- have not been found to be correlated with higher correctness. Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies? Also, Haskell's type system is certainly more expressive and strong than Java's or Python's.
- pittma 7y ago
  > Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies? On the contrary! Consider for instance: "Total Haskell is Reasonable Coq"[1] 1. https://arxiv.org/abs/1711.09286 https://arxiv.org/abs/1711.09286
  - pron 7y ago
    This has absolutely no bearing on the matter. The fact that some simple propositional logic statements could be proven using Haskell if Haskell were total, does not mean it has a significant impact on correctness (which requires predicate logic) even if Haskell were total, and it certainly doesn't mean that it's more effective at increasing correctness than Python. And, BTW, Coq is not a particularly effective tool for writing correct software, either. The largest software whose correctness was largely verified in Coq (CompCert) is positively tiny compared to standard software (it's less than 1/5th of jQuery), and the cost was huge. So Coq's "correctness score" of increased correctness per unit of effort is not particularly stellar compared to alternatives.
- derefr 7y ago
  > unless the spec has undefined behaviour (why would it?) If your code relies on e.g. integer wrapping as implemented by CPU integer instructions, then your code, by design, inherently has undefined behavior for architectures that implement CPU integers using something other than two's-complement. (A lot of crypto code is invalid on these architectures!)
  - csande17 7y ago
    If your code relies on twos-complement integer arithmetic wrapping, you should use a function/operator/language that guarantees that behavior. Then, the function/compiler/interpreter can use the CPU instruction on platforms where it exists and emulate it otherwise.
    - 7y ago
jdc 7y ago
Which languages would you say have expressively "strong" type systems?
- pron 7y ago
  Agda. ATS. Idris. Liquid Haskell would be medium-strength.
swsieber 7y ago
> java Java does not enforce thread safety at compile time. I would take Rust over java just for that. Disclaimer - work heavily in Java by day, and have written some cli tools in Rust.
- pron 7y ago
  Rust doesn't enforce "thread safety" just a lack of a simple kind of data races. Much of it is because data races could result in undefined behavior in Rust when there's a race between freeing memory and accessing it. This kind of race cannot happen in Java, either.
Sharlin 7y ago
Lack of undefined behavior may be a rather low bar to clear with respect to functional correctness, but it absolutely is a bar you have to clear. A program with undefined behavior is trivially not compliant with the specification. Furthermore, Rust's type system is absolutely not only designed to prevent undefined behavior. Dereferencing a null reference in Java or C# is not undefined behavior, but it is still a (tremendously common) bug. Deferencing a null reference in Rust is not possible because null references do not exist. Affine typing allows Rust programs to statically guarantee that only routines applicable to an object's current state can be invoked; in most other languages this can only be checked via runtime assertions. Unique ownership not only guarantees lack of data races but allows programs to statically prevent race conditions more generally, including those that in other languages may occur even in the absence of any concurrency (see eg. Java's ConcurrentModificationException). Rust enums and exhaustive pattern matching statically ensures that all possible values of a type are accounted for. Again, not doing so might not directly lead to undefined behavior, but would be a compliance failure nonetheless, and again, Rust has your back there.
- zozbot234 7y ago
  > but allows programs to statically prevent race conditions more generally Wrong, wrong, wrong! A race condition is an error in program logic. It can't be prevented by a type system, which is limited to local, syntax-based analysis. Race conditions can trivially occur, e.g. in channel- or message-passing-based models of concurrency, where there's nothing that could cause a data race.
  - phamilton 7y ago
    Do linear and/or dependent types change this statement?
    - imtringued 7y ago
      You can always write nonsensical code like this (pseudocode): def counter = 0 def increment() { def tempcounter = null counter.lock { tempcounter = counter } tempcounter++ counter.lock { counter = tempcounter } } Exclusive access to counter is guaranteed and therefore memory safety has been maintained but reads and writes may still be interleaved and cause incorrect results.
agentultra 7y ago
Have you read Ghosts of Departed Proofs? I agree there haven’t been enough studies. Sufficiently advanced type systems do enable us to express specifications that can check our implementation. It’s not on the level of model checkers or proof assistants but it is an awfully effective tool for constructing programs that are functionally correct with respect to their specification, faster.
- pron 7y ago
  Yes, I have, but the question here isn't whether types can be used to verify any correctness property, but whether, overall, there is some correlation between the type system and functional correctness, and there doesn't seem to be one. The question is why this is the case. Perhaps it is because types are not any more effective in their cost/benefit than other ways of increasing correctness. Papers like that are driven by what can be verified with a chosen approach, not by cost/benefit and comparison with other approaches. In other words, they show some property without assigning it a relative value. Pointing at such papers when discussing correctness relative to other languages is like telling people they'd be much better off working at company A rather than company B, because company A gives out free lunches. Even if company B doesn't, it might offer free dinner, and even if it doesn't the salary can be higher, and even if not, it's unclear how big of a difference A's lunch is. In other words, correctness is very complicated, and there is just no way to look at one property or another and make a conclusion. Indeed, there does not seem to be a big difference in practice.
  - agentultra 7y ago
    In the absence of enough studies I find it difficult to draw any hard conclusions. I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows.
    - pron 7y ago
      > In the absence of enough studies I find it difficult to draw any hard conclusions. Me too, which is why I say that it does not seem to make a big positive or negative difference (big differences are easy to find; there haven't been enough studies about the correlation between eating lettuce and baldness so we cannot draw any hard conclusion about there being a correlation or not, and should continue assuming that it's likely not a big cause for baldness nor a definitive cure). > I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows. I agree. Haskell's type system is OK, and I think most other languages also strike a balance that is roughly equally good, albeit not necessarily through the type system, which is why Haskell doesn't appear to be doing much worse or much better at the bottom line. So I definitely see no good reason to suggest Haskell should lead to drastically lower correctness, and if someone said they cared about correctness and want to use Haskell, I wouldn't think it's an exceptionally bad choice. I think (simple) type systems have many good benefits (code organization, documentation, tooling, AOT-compilation performance), which is why I like them, but correctness just isn't one of them. And why should it be? Theory certainly does not suggest simple types should have a big impact on correctness. The strength of the Haskell type system is such that for most uses of it, for any well-typed Haskell program, there is a very small finite-state program that satisfies the same type (expressible as a very small program), yet clearly most of what the program does -- as well as its code -- lies well beyond its type-equivalent small FSM. So any argument that says that the type would still have a big impact of correctness despite the theory saying it shouldn't would also need to explain why other techniques, like tests without a type system, aren't at least as effective (cost/benefit-wise).
mcqueenjordan 7y ago
Isn't safety actually part of functional correctness? Safety is inherently a part of accurately implementing a program's specification, even if it's not always obvious. For example, a 1-in-a-billion race condition can invalidate the functional correctness of a program, and (Type|Memory) safety is one piece of preventing these types of errors.
- pron 7y ago
  I don't understand this argument. Most other languages also give you safety from undefined behavior. Also, an undefined behavior bug is not necessarily more severe than a logic bug.
  - mcqueenjordan 7y ago
    Undefined behavior is different from data races and memory safety bugs, though, right? I'm not saying it's more severe, but it's definitely part of the puzzle.
Too 7y ago
The type system of Rust does so much more than just ensure "undefined-behavior-safety" and increased type safety of any language often does wonders to improve functional correctness. If i had a penny for every time someone forgot to check the return code or errno in a C program i would be a millionaire by now. Such class of error is simply not possible in Rust's type system. I'd classify this error as functional correctness, it has absolutely nothing to do with undefined behavior or anything like that, hence Rust does improve functional correctness. Other common error i see i C# for example is that because of the GC everybody just passes objects around wildly without thinking of ownership, eventually there is a reference to some object everywhere, often in multiple threads, and you have no idea who is the real owner and who is just borrowing. Every reference is mutable so it is often very difficult to understand who is mutating it. Rust's immutability by default with only one mutating reference allowed at a time, would prevent this class of error also. (This isn't necessarily an error in itself but usually this spaghetti eventually leads to functional errors) I do see your point though and agree that it would be very interesting to see a statistical evidence of how well this translates to productivity and end user perceived functional correctness. It could for example be that all such errors are weeded out during testing anyway, which leads us down the endless rabbit hole debate of dynamic vs static programming language. Though in my experience the closer to compilation you can find an error the better. Especially in larger teams where types not only help yourself but also describe the intent of the code for others.
- pron 7y ago
  > I'd classify this error as functional correctness It isn't. Functional correctness is about ensuring that the code matches the spec. Preventing those kind of bugs could have a positive or a negative impact on functional correctness, but they are not, in themselves, functional bugs. > Such class of error is simply not possible in Rust's type system. This doesn't have much to do with correctness, though, and it's is a common mistake when discussing correctness (a subject I have written extensively about https://pron.github.io/ https://pron.github.io/). I am not saying that eliminating a certain class of bugs is bad; it might actually be good (although it might also be bad), but it's far from simple. It is absolutely not the case that if one language eliminates a certain class of bugs and another one doesn't, then the first leads to more correct programs. This implication is just wrong, both in its internal logic as well as empirically. To get some intuition for why it's wrong, consider that when naively writing a program on paper, you introduce 100 bugs. When you actually program it, you must use a variety of methods, including tests to get rid of them. Now, if you use a language that eliminates 10 of them with its type system, it does not mean that given the same amount of effort, you'll catch more bugs in that language than the other. It's possible (indeed, we know it happens when we work with more powerful type systems like dependent types) that it's harder to write the program in the first language, and in the time it took you to eliminate those 10 bugs -- i.e. getting the program to compile -- you'll have found 20 in the other language. And it's certainly possible that overall there just wouldn't be much difference. Again, I am not saying eliminating certain classes of bugs is bad. I am saying that it is absolutely not true that doing so is a certain path to better correctness. In any event, Rust's type system does not directly increase functional correctness. It does eliminate some bugs that could cause functional correctness issues, but whether the approach's cost/benefit is significantly better or significantly worse than, say, Java or Python is very, very far from clear.
thesz 7y ago
The goal of Haskell type system is to have Rust as a library. For example: http://hackage.haskell.org/package/liboleg-2010.1.10.0/docs/System-SafeHandles.html http://hackage.haskell.org/package/liboleg-2010.1.10.0/docs/... One can implement linear types and Rust's borrow checker in the Haskell as a DSL. That's main difference - in Haskell, you describe a system where different parts have different properties and use type checked DSLs to express them and type checker to ensure that everything goes along well.

by pron 7y ago

NOGDP 7y ago

> the term normally refers to functional correctness, i.e. that the program satisfies the specification, not that it doesn't have undefined behavior A program that has undefined behaviour is not correct, unless the spec has undefined behaviour (why would it?). > On that front, there seems to be no evidence, nor even hints, that either Haskell or Rust achieve better correctness (or the same correctness more cheaply). I don't know what you mean by evidence, but Haskell has a stronger and more expressive type system than say Java, it doesn't have null pointers, it has referential transparency, and simpler, safer concurrency and parallelism builtins. The fact that you can make more general assumptions about pieces of code which you don't necessarily fully understand makes writing safer and correct code easier. > But Rust's type system, and certainly Haskell's -- both interesting but very expressively "weak" type systems -- have not been found to be correlated with higher correctness. Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies? Also, Haskell's type system is certainly more expressive and strong than Java's or Python's.

pittma 7y ago
> Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies? On the contrary! Consider for instance: "Total Haskell is Reasonable Coq"[1] 1. https://arxiv.org/abs/1711.09286 https://arxiv.org/abs/1711.09286
- pron 7y ago
  This has absolutely no bearing on the matter. The fact that some simple propositional logic statements could be proven using Haskell if Haskell were total, does not mean it has a significant impact on correctness (which requires predicate logic) even if Haskell were total, and it certainly doesn't mean that it's more effective at increasing correctness than Python. And, BTW, Coq is not a particularly effective tool for writing correct software, either. The largest software whose correctness was largely verified in Coq (CompCert) is positively tiny compared to standard software (it's less than 1/5th of jQuery), and the cost was huge. So Coq's "correctness score" of increased correctness per unit of effort is not particularly stellar compared to alternatives.
derefr 7y ago
> unless the spec has undefined behaviour (why would it?) If your code relies on e.g. integer wrapping as implemented by CPU integer instructions, then your code, by design, inherently has undefined behavior for architectures that implement CPU integers using something other than two's-complement. (A lot of crypto code is invalid on these architectures!)
- csande17 7y ago
  If your code relies on twos-complement integer arithmetic wrapping, you should use a function/operator/language that guarantees that behavior. Then, the function/compiler/interpreter can use the CPU instruction on platforms where it exists and emulate it otherwise.
  - 7y ago

jdc 7y ago

Which languages would you say have expressively "strong" type systems?

pron 7y ago
Agda. ATS. Idris. Liquid Haskell would be medium-strength.

swsieber 7y ago

> java Java does not enforce thread safety at compile time. I would take Rust over java just for that. Disclaimer - work heavily in Java by day, and have written some cli tools in Rust.

pron 7y ago
Rust doesn't enforce "thread safety" just a lack of a simple kind of data races. Much of it is because data races could result in undefined behavior in Rust when there's a race between freeing memory and accessing it. This kind of race cannot happen in Java, either.

Sharlin 7y ago

Lack of undefined behavior may be a rather low bar to clear with respect to functional correctness, but it absolutely is a bar you have to clear. A program with undefined behavior is trivially not compliant with the specification. Furthermore, Rust's type system is absolutely not only designed to prevent undefined behavior. Dereferencing a null reference in Java or C# is not undefined behavior, but it is still a (tremendously common) bug. Deferencing a null reference in Rust is not possible because null references do not exist. Affine typing allows Rust programs to statically guarantee that only routines applicable to an object's current state can be invoked; in most other languages this can only be checked via runtime assertions. Unique ownership not only guarantees lack of data races but allows programs to statically prevent race conditions more generally, including those that in other languages may occur even in the absence of any concurrency (see eg. Java's ConcurrentModificationException). Rust enums and exhaustive pattern matching statically ensures that all possible values of a type are accounted for. Again, not doing so might not directly lead to undefined behavior, but would be a compliance failure nonetheless, and again, Rust has your back there.

zozbot234 7y ago
> but allows programs to statically prevent race conditions more generally Wrong, wrong, wrong! A race condition is an error in program logic. It can't be prevented by a type system, which is limited to local, syntax-based analysis. Race conditions can trivially occur, e.g. in channel- or message-passing-based models of concurrency, where there's nothing that could cause a data race.
- phamilton 7y ago
  Do linear and/or dependent types change this statement?
  - imtringued 7y ago
    You can always write nonsensical code like this (pseudocode): def counter = 0 def increment() { def tempcounter = null counter.lock { tempcounter = counter } tempcounter++ counter.lock { counter = tempcounter } } Exclusive access to counter is guaranteed and therefore memory safety has been maintained but reads and writes may still be interleaved and cause incorrect results.

agentultra 7y ago

Have you read Ghosts of Departed Proofs? I agree there haven’t been enough studies. Sufficiently advanced type systems do enable us to express specifications that can check our implementation. It’s not on the level of model checkers or proof assistants but it is an awfully effective tool for constructing programs that are functionally correct with respect to their specification, faster.

pron 7y ago
Yes, I have, but the question here isn't whether types can be used to verify any correctness property, but whether, overall, there is some correlation between the type system and functional correctness, and there doesn't seem to be one. The question is why this is the case. Perhaps it is because types are not any more effective in their cost/benefit than other ways of increasing correctness. Papers like that are driven by what can be verified with a chosen approach, not by cost/benefit and comparison with other approaches. In other words, they show some property without assigning it a relative value. Pointing at such papers when discussing correctness relative to other languages is like telling people they'd be much better off working at company A rather than company B, because company A gives out free lunches. Even if company B doesn't, it might offer free dinner, and even if it doesn't the salary can be higher, and even if not, it's unclear how big of a difference A's lunch is. In other words, correctness is very complicated, and there is just no way to look at one property or another and make a conclusion. Indeed, there does not seem to be a big difference in practice.
- agentultra 7y ago
  In the absence of enough studies I find it difficult to draw any hard conclusions. I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows.
  - pron 7y ago
    > In the absence of enough studies I find it difficult to draw any hard conclusions. Me too, which is why I say that it does not seem to make a big positive or negative difference (big differences are easy to find; there haven't been enough studies about the correlation between eating lettuce and baldness so we cannot draw any hard conclusion about there being a correlation or not, and should continue assuming that it's likely not a big cause for baldness nor a definitive cure). > I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows. I agree. Haskell's type system is OK, and I think most other languages also strike a balance that is roughly equally good, albeit not necessarily through the type system, which is why Haskell doesn't appear to be doing much worse or much better at the bottom line. So I definitely see no good reason to suggest Haskell should lead to drastically lower correctness, and if someone said they cared about correctness and want to use Haskell, I wouldn't think it's an exceptionally bad choice. I think (simple) type systems have many good benefits (code organization, documentation, tooling, AOT-compilation performance), which is why I like them, but correctness just isn't one of them. And why should it be? Theory certainly does not suggest simple types should have a big impact on correctness. The strength of the Haskell type system is such that for most uses of it, for any well-typed Haskell program, there is a very small finite-state program that satisfies the same type (expressible as a very small program), yet clearly most of what the program does -- as well as its code -- lies well beyond its type-equivalent small FSM. So any argument that says that the type would still have a big impact of correctness despite the theory saying it shouldn't would also need to explain why other techniques, like tests without a type system, aren't at least as effective (cost/benefit-wise).

mcqueenjordan 7y ago

Isn't safety actually part of functional correctness? Safety is inherently a part of accurately implementing a program's specification, even if it's not always obvious. For example, a 1-in-a-billion race condition can invalidate the functional correctness of a program, and (Type|Memory) safety is one piece of preventing these types of errors.

pron 7y ago
I don't understand this argument. Most other languages also give you safety from undefined behavior. Also, an undefined behavior bug is not necessarily more severe than a logic bug.
- mcqueenjordan 7y ago
  Undefined behavior is different from data races and memory safety bugs, though, right? I'm not saying it's more severe, but it's definitely part of the puzzle.

Too 7y ago

The type system of Rust does so much more than just ensure "undefined-behavior-safety" and increased type safety of any language often does wonders to improve functional correctness. If i had a penny for every time someone forgot to check the return code or errno in a C program i would be a millionaire by now. Such class of error is simply not possible in Rust's type system. I'd classify this error as functional correctness, it has absolutely nothing to do with undefined behavior or anything like that, hence Rust does improve functional correctness. Other common error i see i C# for example is that because of the GC everybody just passes objects around wildly without thinking of ownership, eventually there is a reference to some object everywhere, often in multiple threads, and you have no idea who is the real owner and who is just borrowing. Every reference is mutable so it is often very difficult to understand who is mutating it. Rust's immutability by default with only one mutating reference allowed at a time, would prevent this class of error also. (This isn't necessarily an error in itself but usually this spaghetti eventually leads to functional errors) I do see your point though and agree that it would be very interesting to see a statistical evidence of how well this translates to productivity and end user perceived functional correctness. It could for example be that all such errors are weeded out during testing anyway, which leads us down the endless rabbit hole debate of dynamic vs static programming language. Though in my experience the closer to compilation you can find an error the better. Especially in larger teams where types not only help yourself but also describe the intent of the code for others.

pron 7y ago
> I'd classify this error as functional correctness It isn't. Functional correctness is about ensuring that the code matches the spec. Preventing those kind of bugs could have a positive or a negative impact on functional correctness, but they are not, in themselves, functional bugs. > Such class of error is simply not possible in Rust's type system. This doesn't have much to do with correctness, though, and it's is a common mistake when discussing correctness (a subject I have written extensively about https://pron.github.io/ https://pron.github.io/). I am not saying that eliminating a certain class of bugs is bad; it might actually be good (although it might also be bad), but it's far from simple. It is absolutely not the case that if one language eliminates a certain class of bugs and another one doesn't, then the first leads to more correct programs. This implication is just wrong, both in its internal logic as well as empirically. To get some intuition for why it's wrong, consider that when naively writing a program on paper, you introduce 100 bugs. When you actually program it, you must use a variety of methods, including tests to get rid of them. Now, if you use a language that eliminates 10 of them with its type system, it does not mean that given the same amount of effort, you'll catch more bugs in that language than the other. It's possible (indeed, we know it happens when we work with more powerful type systems like dependent types) that it's harder to write the program in the first language, and in the time it took you to eliminate those 10 bugs -- i.e. getting the program to compile -- you'll have found 20 in the other language. And it's certainly possible that overall there just wouldn't be much difference. Again, I am not saying eliminating certain classes of bugs is bad. I am saying that it is absolutely not true that doing so is a certain path to better correctness. In any event, Rust's type system does not directly increase functional correctness. It does eliminate some bugs that could cause functional correctness issues, but whether the approach's cost/benefit is significantly better or significantly worse than, say, Java or Python is very, very far from clear.

thesz 7y ago

The goal of Haskell type system is to have Rust as a library. For example: http://hackage.haskell.org/package/liboleg-2010.1.10.0/docs/System-SafeHandles.html http://hackage.haskell.org/package/liboleg-2010.1.10.0/docs/... One can implement linear types and Rust's borrow checker in the Haskell as a DSL. That's main difference - in Haskell, you describe a system where different parts have different properties and use type checked DSLs to express them and type checker to ensure that everything goes along well.