5 ms·

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

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.
    - phamilton 7y ago
      Your point is a good one: a correct program might still be wrong. I think the argument is that it's inadequately typed. I.e. the program itself is correct because the semantics aren't captured properly. If you had a type system that captured that tempcounter was derived from an earlier version of counter, then it could enforce that the assignment of counter in the second lock does not depend on a previous version of counter. Runtime enforcement would be trivial in most languages by making counter a monad that essentially carried a DAG around to detect this sort of problem. I'm pretty sure though that you could enforce this at compile time with dependent types in something like Idris.
- Sharlin 7y ago
  Wrong, wrong, wrong. As I said, race conditions caused by non-exclusive mutable access (such as modifying a collection while iterating over it) are trivially prevented by forbidding non-exclusive mutable access! Which is what Rust does. Not all race conditions can be prevented, obviously. But that does not mean that none of them can. I'm not sure what you mean by "local, syntax-based analysis" given that type systems are neither local nor syntax-based. Do you perhaps have a failure of imagination of what sorts of invariants a powerful type system is able to enforce?
SamReidHughes 7y ago
The point about null references is a very good example. In both Rust and GC'd languages whose type system differentiates between null and non-null pointer types, it is impossible to define a type like Vector<T>, where T doesn't have a default constructor, without resorting to some form of type cast. In Rust, as well as GC'd languages like TypeScript, dereferencing a null reference is possible, in the same sense, because a type cast or unsafe code may have been incorrect.
- Filligree 7y ago
  > In Rust, as well as GC'd languages like TypeScript, dereferencing a null reference is possible, in the same sense, because a type cast or unsafe code may have been incorrect. True, but type casts are unsafe code. You'll never see a null pointer so long as you stick to the safe language subset.
pron 7y ago
> but it absolutely is a bar you have to clear. I don't think that a program must be free of undefined behavior before significantly reducing bugs. I think most people would prefer a program with five undefined behavior bugs and no other bugs to a program with zero undefined behaviors but 50 other bugs (assuming all those bugs are of similar severity). Also, even clearing that bar doesn't require doing so with the type system (e.g. Python doesn't have undefined behavior, either). It also doesn't mean that clearing it gets you very far with respect to functional correctness. > 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. Yes, but that doesn't mean that the end result is more correct, and, indeed, there is no evidence to suggest that it is. Software correctness is an extremely complicated topic, one that I have written extensively about [1], and just pointing out that one technique can eliminate a certain class of bugs is almost never a guarantee that that technique is superior to other techniques, even if they are partial. [1]: https://pron.github.io/ https://pron.github.io/
- pmoriarty 7y ago
  "Also, even clearing that bar doesn't require doing so with the type system (e.g. Python doesn't have undefined behavior, either)." If python doesn't have a type system, why does it report type errors like this? >>> "foo" / "bar" Traceback (most recent call last): File "<stdin>", line 1, in <module> TypeError: unsupported operand type(s) for /: 'str' and 'str'
  - pron 7y ago
    In programming language theory and formal systems in general, "types" mean what is often called "static types." In any event, that's what I'm referring to.
  - deleted 7y ago
    [deleted]
- im_down_w_otp 7y ago
  In the places where correctness tends to matter, like safety-critical domains, undefined behavior is unquestionably worse. It's open ended latent risk and also impacts the soundness of attempts to deal with residual risk. Depending on the nature and surface area of the undefined behavior, you can't necessarily know that your program has "no other bugs" if you can't trust the soundness of the rules for writing your program to begin with. You'll have to test it externally with something that you can depend on the soundness of, which is just moving the same work to somewhere else.
kyllo 7y ago
> A program with undefined behavior is trivially not compliant with the specification. Undefined behavior means doing something the compiler spec does not specify, therefore the compiler is free to do anything. There are plenty of programs that exploit the programmer's knowledge of a particular compiler's actual, unspecified behavior as an optimization. One example is using an int variable after an overflow. Post-overflow, the int's value is undefined behavior, but in practice it is predictable for a given compiler and platform. It is possible to write a program that implements its own program spec correctly, while exploiting out-of-spec behavior of its compiler under the hood. Much like how it's possible to wrap unsafe Rust code with a safe interface.
- fulafel 7y ago
  It's worth noting that gcc and llvm treat C integer overflow as a can't-happen condition (unless you supply an explicit compiler flag to change overflow semantics).
- Too 7y ago
  Relying on undefined behavior because your compiler happens to behave a certain way today on one specific machine is NOT the same as wrapping unsafe with safe. Next version of the compiler can exploit the undefined behavior and simply remove the code as an optimization, or even worse the optimization is already in your current compiler and only happens under some strange circumstances you are not aware of. Unsafe code blocks still have defined and predictable behavior, but you have to guarantee the memory safety.
- saagarjha 7y ago
  > There are plenty of programs that exploit the programmer's knowledge of a particular compiler's actual, unspecified behavior as an optimization. And then they break when the compiler changes its behavior…
- likeliv 7y ago
  > There are plenty of programs that exploit the programmer's knowledge of a particular compiler's actual, unspecified behavior as an optimization. There are plenty of programs that have bugs. Programmers who exploit undefined behavior on purpose are reckless.

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.
  - phamilton 7y ago
    Your point is a good one: a correct program might still be wrong. I think the argument is that it's inadequately typed. I.e. the program itself is correct because the semantics aren't captured properly. If you had a type system that captured that tempcounter was derived from an earlier version of counter, then it could enforce that the assignment of counter in the second lock does not depend on a previous version of counter. Runtime enforcement would be trivial in most languages by making counter a monad that essentially carried a DAG around to detect this sort of problem. I'm pretty sure though that you could enforce this at compile time with dependent types in something like Idris.
Sharlin 7y ago
Wrong, wrong, wrong. As I said, race conditions caused by non-exclusive mutable access (such as modifying a collection while iterating over it) are trivially prevented by forbidding non-exclusive mutable access! Which is what Rust does. Not all race conditions can be prevented, obviously. But that does not mean that none of them can. I'm not sure what you mean by "local, syntax-based analysis" given that type systems are neither local nor syntax-based. Do you perhaps have a failure of imagination of what sorts of invariants a powerful type system is able to enforce?

SamReidHughes 7y ago

The point about null references is a very good example. In both Rust and GC'd languages whose type system differentiates between null and non-null pointer types, it is impossible to define a type like Vector<T>, where T doesn't have a default constructor, without resorting to some form of type cast. In Rust, as well as GC'd languages like TypeScript, dereferencing a null reference is possible, in the same sense, because a type cast or unsafe code may have been incorrect.

Filligree 7y ago
> In Rust, as well as GC'd languages like TypeScript, dereferencing a null reference is possible, in the same sense, because a type cast or unsafe code may have been incorrect. True, but type casts are unsafe code. You'll never see a null pointer so long as you stick to the safe language subset.

pron 7y ago

> but it absolutely is a bar you have to clear. I don't think that a program must be free of undefined behavior before significantly reducing bugs. I think most people would prefer a program with five undefined behavior bugs and no other bugs to a program with zero undefined behaviors but 50 other bugs (assuming all those bugs are of similar severity). Also, even clearing that bar doesn't require doing so with the type system (e.g. Python doesn't have undefined behavior, either). It also doesn't mean that clearing it gets you very far with respect to functional correctness. > 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. Yes, but that doesn't mean that the end result is more correct, and, indeed, there is no evidence to suggest that it is. Software correctness is an extremely complicated topic, one that I have written extensively about [1], and just pointing out that one technique can eliminate a certain class of bugs is almost never a guarantee that that technique is superior to other techniques, even if they are partial. [1]: https://pron.github.io/ https://pron.github.io/

pmoriarty 7y ago
"Also, even clearing that bar doesn't require doing so with the type system (e.g. Python doesn't have undefined behavior, either)." If python doesn't have a type system, why does it report type errors like this? >>> "foo" / "bar" Traceback (most recent call last): File "<stdin>", line 1, in <module> TypeError: unsupported operand type(s) for /: 'str' and 'str'
- pron 7y ago
  In programming language theory and formal systems in general, "types" mean what is often called "static types." In any event, that's what I'm referring to.
- deleted 7y ago
  [deleted]
im_down_w_otp 7y ago
In the places where correctness tends to matter, like safety-critical domains, undefined behavior is unquestionably worse. It's open ended latent risk and also impacts the soundness of attempts to deal with residual risk. Depending on the nature and surface area of the undefined behavior, you can't necessarily know that your program has "no other bugs" if you can't trust the soundness of the rules for writing your program to begin with. You'll have to test it externally with something that you can depend on the soundness of, which is just moving the same work to somewhere else.

kyllo 7y ago

> A program with undefined behavior is trivially not compliant with the specification. Undefined behavior means doing something the compiler spec does not specify, therefore the compiler is free to do anything. There are plenty of programs that exploit the programmer's knowledge of a particular compiler's actual, unspecified behavior as an optimization. One example is using an int variable after an overflow. Post-overflow, the int's value is undefined behavior, but in practice it is predictable for a given compiler and platform. It is possible to write a program that implements its own program spec correctly, while exploiting out-of-spec behavior of its compiler under the hood. Much like how it's possible to wrap unsafe Rust code with a safe interface.

fulafel 7y ago
It's worth noting that gcc and llvm treat C integer overflow as a can't-happen condition (unless you supply an explicit compiler flag to change overflow semantics).
Too 7y ago
Relying on undefined behavior because your compiler happens to behave a certain way today on one specific machine is NOT the same as wrapping unsafe with safe. Next version of the compiler can exploit the undefined behavior and simply remove the code as an optimization, or even worse the optimization is already in your current compiler and only happens under some strange circumstances you are not aware of. Unsafe code blocks still have defined and predictable behavior, but you have to guarantee the memory safety.
saagarjha 7y ago
> There are plenty of programs that exploit the programmer's knowledge of a particular compiler's actual, unspecified behavior as an optimization. And then they break when the compiler changes its behavior…
likeliv 7y ago
> There are plenty of programs that exploit the programmer's knowledge of a particular compiler's actual, unspecified behavior as an optimization. There are plenty of programs that have bugs. Programmers who exploit undefined behavior on purpose are reckless.