5 ms·

> 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

by 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.
  - derefr 7y ago
    Sure. Can you name the relevant intrinsic in any pre-modern language? It's nice that Rust has overflowing_add, but what were you supposed to do in the 90s? GCC's __builtin_add_overflow only appeared in 2014. Before that, there was this: http://kqueue.org/blog/2012/03/16/fast-integer-overflow-detection/ http://kqueue.org/blog/2012/03/16/fast-integer-overflow-dete..., where, hilariously: > GCC will optimize away the check (c < 0) ...and the suggested solution to this was to use special, third-party "safe math" libraries written in target-specific assembly. Which meant you weren't really getting the feature we're looking for (which is portable code that will compile anywhere, using either native two's-complement wrapping arith when available, or a shimmed emulation of it when not), because you were locking yourself into a whitelist of targets that the library had been written to support. Now, mind you, that's just C. "Using two's complement arithmetic" might be something you can get a guarantee on from, say, Ada, or Fortran, but if you can, I've never heard about it. Anyone know?
  - kyllo 7y ago
    Optimization often requires knowledge of the behavior at a level of abstraction lower than the one you're currently working at, and exploiting leaky abstractions. Taking away the assumption of two's complement makes code more portable at the cost of making a lot of optimizations impossible. It's a tradeoff, not an absolute rule. As soon as undefined behavior is guaranteed by a spec, it's no longer undefined, so your statement reduces to "you should never rely on UB." You can say that, but people will still do it because it makes their programs faster.
jcranmer 7y ago
> unless the spec has undefined behaviour (why would it?). Because maybe you're specifying a partial function. The code to handle the special cases of invalid inputs can sometimes have dramatic effects on code size and performance, sometimes too much to bear for code that should never run in the first place; allowing for garbage output to be produced for garbage input instead of a result that says "this is garbage input" could well be acceptable. Furthermore, there are some places where we don't actually know how to specify the intended behavior in the first place. Data races are perhaps the best example here; we have yet to find a satisfying specification for data races that is more constraining than "anything goes," and the two most well-known attempts (Java and C++) have both been widely regarded as failures. But pointer aliasing is another area that proves surprisingly difficult: if requiring pointer provenance isn't acceptable, then trying to come up with a reasonable specification is surprisingly difficult.
- amluto 7y ago
  Would pointer provenance still be such a big deal if one-past-the-end pointers were disallowed? All the interesting examples I’ve seen are based on one-past-the-end pointers. I assume something analogous could happen with pointers to freed memory that are converted to integers, but that seems easier to resolve.
- NOGDP 7y ago
  > The code to handle the special cases of invalid inputs can sometimes have dramatic effects on code size and performance, sometimes too much to bear for code that should never run in the first place; allowing for garbage output to be produced for garbage input instead of a result that says "this is garbage input" could well be acceptable. That seems solvable by refactoring your types a little. Also, some languages do not allow partial functions - such as total functional programming languages. > we have yet to find a satisfying specification for data races that is more constraining than "anything goes," and the two most well-known attempts (Java and C++) have both been widely regarded as failures. What about nested data parallelism[1] or pure parallelism such as in Haskell? [1] https://www.classes.cs.uchicago.edu/archive/2016/winter/32001-1/papers/nepal.pdf https://www.classes.cs.uchicago.edu/archive/2016/winter/3200...
gambler 7y ago
>I don't know what you mean by evidence, but Haskell has a stronger and more expressive type system than say Java My first experience with running real Haskell code was installing Leksah - which is a Haskell editor written in Haskell itself. I initially installed an older version by accident. It presented me with some window saying it will try to download something. Then it closed spewing a cryptic error message into the console. I could not restart it, because the program immediately went to the same error on startup. I then installed the latest version. That one loaded... only to consistently crash when I tried to create a file. This is what happens when software is written by people who don't understand the difference between theoretical "correctness" and real-life reliability.
pron 7y ago
> A program that has undefined behaviour is not correct, unless the spec has undefined behaviour (why would it?). Yes, but a program has many ways in which it cannot be correct, and eliminating one of them does not mean that you've eliminated a significant amount of problems, and it doesn't even mean that the amount of incorrectness you've eliminated is bigger if you'd spent your time with other approaches. > 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. Except this does not seem to be the case, as evidence does not suggest that Haskell programs have significantly fewer bugs or are produced faster. > 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? I am saying that there is no evidence to suggest Haskell programs are more correct, and that at least one study has tried to find such correlation but did not. > Also, Haskell's type system is certainly more expressive and strong than Java's or Python's. It is, but it is still very weak.
- NOGDP 7y ago
  > Except this does not seem to be the case, as evidence does not suggest that Haskell programs have significantly fewer bugs or are produced faster. What evidence? > It is, but it is still very weak. It's strong relative to the most popular programming languages in use today.
  - pron 7y ago
    > What evidence? Similar evidence to that that does not suggest eating lettuce reduces baldness. > It's strong relative to the most popular programming languages in use today. On an expressivity scale, as far as functional correctness is concerned, if Python is 1, Java is 2 and Agda is 100, Haskell would be at maybe 2.5. Sure, stronger, but not enough to suggest it has some real impact, and, indeed, none has so far been found.
    - charlieflowers 7y ago
      Interesting. What are some other languages that would be above 2.5 on your scale?

by NOGDP 7y ago

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.
- derefr 7y ago
  Sure. Can you name the relevant intrinsic in any pre-modern language? It's nice that Rust has overflowing_add, but what were you supposed to do in the 90s? GCC's __builtin_add_overflow only appeared in 2014. Before that, there was this: http://kqueue.org/blog/2012/03/16/fast-integer-overflow-detection/ http://kqueue.org/blog/2012/03/16/fast-integer-overflow-dete..., where, hilariously: > GCC will optimize away the check (c < 0) ...and the suggested solution to this was to use special, third-party "safe math" libraries written in target-specific assembly. Which meant you weren't really getting the feature we're looking for (which is portable code that will compile anywhere, using either native two's-complement wrapping arith when available, or a shimmed emulation of it when not), because you were locking yourself into a whitelist of targets that the library had been written to support. Now, mind you, that's just C. "Using two's complement arithmetic" might be something you can get a guarantee on from, say, Ada, or Fortran, but if you can, I've never heard about it. Anyone know?
- kyllo 7y ago
  Optimization often requires knowledge of the behavior at a level of abstraction lower than the one you're currently working at, and exploiting leaky abstractions. Taking away the assumption of two's complement makes code more portable at the cost of making a lot of optimizations impossible. It's a tradeoff, not an absolute rule. As soon as undefined behavior is guaranteed by a spec, it's no longer undefined, so your statement reduces to "you should never rely on UB." You can say that, but people will still do it because it makes their programs faster.

jcranmer 7y ago

> unless the spec has undefined behaviour (why would it?). Because maybe you're specifying a partial function. The code to handle the special cases of invalid inputs can sometimes have dramatic effects on code size and performance, sometimes too much to bear for code that should never run in the first place; allowing for garbage output to be produced for garbage input instead of a result that says "this is garbage input" could well be acceptable. Furthermore, there are some places where we don't actually know how to specify the intended behavior in the first place. Data races are perhaps the best example here; we have yet to find a satisfying specification for data races that is more constraining than "anything goes," and the two most well-known attempts (Java and C++) have both been widely regarded as failures. But pointer aliasing is another area that proves surprisingly difficult: if requiring pointer provenance isn't acceptable, then trying to come up with a reasonable specification is surprisingly difficult.

amluto 7y ago
Would pointer provenance still be such a big deal if one-past-the-end pointers were disallowed? All the interesting examples I’ve seen are based on one-past-the-end pointers. I assume something analogous could happen with pointers to freed memory that are converted to integers, but that seems easier to resolve.
NOGDP 7y ago
> The code to handle the special cases of invalid inputs can sometimes have dramatic effects on code size and performance, sometimes too much to bear for code that should never run in the first place; allowing for garbage output to be produced for garbage input instead of a result that says "this is garbage input" could well be acceptable. That seems solvable by refactoring your types a little. Also, some languages do not allow partial functions - such as total functional programming languages. > we have yet to find a satisfying specification for data races that is more constraining than "anything goes," and the two most well-known attempts (Java and C++) have both been widely regarded as failures. What about nested data parallelism[1] or pure parallelism such as in Haskell? [1] https://www.classes.cs.uchicago.edu/archive/2016/winter/32001-1/papers/nepal.pdf https://www.classes.cs.uchicago.edu/archive/2016/winter/3200...

gambler 7y ago

>I don't know what you mean by evidence, but Haskell has a stronger and more expressive type system than say Java My first experience with running real Haskell code was installing Leksah - which is a Haskell editor written in Haskell itself. I initially installed an older version by accident. It presented me with some window saying it will try to download something. Then it closed spewing a cryptic error message into the console. I could not restart it, because the program immediately went to the same error on startup. I then installed the latest version. That one loaded... only to consistently crash when I tried to create a file. This is what happens when software is written by people who don't understand the difference between theoretical "correctness" and real-life reliability.

pron 7y ago

> A program that has undefined behaviour is not correct, unless the spec has undefined behaviour (why would it?). Yes, but a program has many ways in which it cannot be correct, and eliminating one of them does not mean that you've eliminated a significant amount of problems, and it doesn't even mean that the amount of incorrectness you've eliminated is bigger if you'd spent your time with other approaches. > 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. Except this does not seem to be the case, as evidence does not suggest that Haskell programs have significantly fewer bugs or are produced faster. > 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? I am saying that there is no evidence to suggest Haskell programs are more correct, and that at least one study has tried to find such correlation but did not. > Also, Haskell's type system is certainly more expressive and strong than Java's or Python's. It is, but it is still very weak.

NOGDP 7y ago
> Except this does not seem to be the case, as evidence does not suggest that Haskell programs have significantly fewer bugs or are produced faster. What evidence? > It is, but it is still very weak. It's strong relative to the most popular programming languages in use today.
- pron 7y ago
  > What evidence? Similar evidence to that that does not suggest eating lettuce reduces baldness. > It's strong relative to the most popular programming languages in use today. On an expressivity scale, as far as functional correctness is concerned, if Python is 1, Java is 2 and Agda is 100, Haskell would be at maybe 2.5. Sure, stronger, but not enough to suggest it has some real impact, and, indeed, none has so far been found.
  - charlieflowers 7y ago
    Interesting. What are some other languages that would be above 2.5 on your scale?