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.
What evidence?
> It is, but it is still very weak.
It's strong relative to the most popular programming languages in use today.
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.
Liquid Haskell would be a big jump (say, to 20), and anything more than that would put you close to, or at, 100.
But note that type systems are far from the only way of expressing correctness properties. Eve is untyped, but its ability to express correctness properties is much higher than Haskell's. Also, even type systems that are designed for functional correctness do not necessarily do a good job at it compared to other approaches.
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.
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/3200...
I assume something analogous could happen with pointers to freed memory that are converted to integers, but that seems easier to resolve.
On the contrary! Consider for instance: "Total Haskell is Reasonable Coq"[1]
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.
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!)
> 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?
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.
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.
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.