Hacker News Reader

> 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.

> 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.

> 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.

Interesting. What are some other languages that would be above 2.5 on your scale?

The jumps in expressivity are not very gradual, and the reason for that is the exact same one as computational expressivity growing "suddenly". PDA's are much more expressive than DFAs, and TM's are drastically more expressive than PDAs.

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.

> 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.

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.

> 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/3200...

> 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

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.

> 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!)

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.

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-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?

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.

I beg to differ. Signed-overflow and such could easily be defined as returning an implementation-defined value. No UB is required.

UB exactly means that it's up to the implementation to decide the behavior because the language spec doesn't. "Implementation-defined" == UB.

No it doesn’t. Implementation-defined means that the implementer must know and document the behaviour (define it). Undefined behaviour may well be behaviour that the implementer does not understand at all (for example it may invoke other undefined behaviour from another part of the system or an underlying system).

No, there's a distinction. "Implementation defined" means that every implementation is free to do what it likes, but it must document what it does. Undefined behavior is illegal to have in your program, period, and means the implementation has no restrictions on what it can do–including being inconsistent.

>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.