Hacker News Reader

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

"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'

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.

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.

Of course, if you want to ensure the correctness of your software using techniques that rely on the lack of undefined behavior in the language then you'd use a language without undefined behavior (although this doesn't require ensuring that in the type system). But that's not usually how it works. Even when using, say, deductive proofs [1], you can prove your program has no undefined behavior -- just as you prove it has no logic bug (with respect to the spec). So it's not worse. To give you an example from mathematics, if you need to prove that, under some conditions, 1/x > 10 knowing x ≥ 0, you'll need to prove that x < 0.1 and that x ≠ 0, and the latter is not "worse" just because 1/0 is not defined while 1/0.1 is, and it's not harder than proving x ≠ 0 when 1/0 is defined (as it is, e.g. in Coq and Isabelle). Similarly, if you want to prove that in, C, a[i] < 10, you will need to prove, among other things, that i ≥ 0 and that i < length of the array, and the fact that a[i] could be undefined if the latter is false does not make that part of the proof harder, nor does it reduce the soundness of the result if it is true.

I.e. the mere existence of undefined behavior in the formal system does not negate the soundness of the entire system. At least it doesn't in arithmetic and it doesn't in C. In fact, C is currently the language with the best formal verification tools. Of course, that is out of necessity, but it's absolutely false that the presence of undefined behavior in the language breaks the possibility of sound formal deductions.

It is true that C does make some local logical inferences more tedious, and some of that is due to undefined behavior, but that's a whole other discussion.

[1]: Deductive proofs are very rarely used in real safety critical system, and they're especially unpopular even compared to other formal methods such as sound static analysis and model checking. Those two are more commonly used in safety critical systems, but the most common assurance tool is tests.

Their popularity has more to do with how the certification regimes are created, which itself has next to nothing to do with the particular efficacy or relative strength of a given verification approach.

I'm also not sure what your disagreeing with exactly. The reason all those assistive tools for C exist is because C is popular for orthogonal reasons, but also its undefined behavior is known to be a source of danger & uncertainty. That's why compilers undergo qualification for instance. The undefined behavior is characterized, catalogued, and codified to turn it into de facto defined behavior.

> The undefined behavior is characterized, catalogued, and codified to turn it into de facto defined behavior.

No, this is not true. Again, the fact that a[i] is undefined for values of i greater than or equal to the array's length does not necessarily make guarantees about the value of a[i] more difficult when it is defined, and it certainly does not impact the soundness in that case. Verification methods can -- and do -- deal with undefinedness without making it "de facto defined". Indeed, even in arithmetics 1/0 is not defined, and yet Peano arithmetics is fine. Formal logic in general does not require every expression to be defined (in the sense of having a certain specific value) in order for it to be sound.

I agree that undefined behavior is a problem, but it is not necessarily worse than other problems when correctness is concerned, and it is not true that it affects the soundness of inferences. It can certainly be tricky or confusing, though, and it is certainly a source of incompatibilities, which is why most languages try to avoid it or control it (Rust has undefined behavior inside unsafe, and Zig can dis/allow it depending on compilation level).

> No, this is not true.

A whole bunch of the tests and the developer interface agreement that come with your purchase of a IEC/ISO qualified C compiler are around establishing what that instance of the compiler does with undefined behavior corners of C. The whole point is to have evidence of turning unknowns into knowns for a defined set of deployment constraints.

> Again, the fact that a[i] is undefined for values of i greater than or equal to the array's length does not necessarily make guarantees about the value of a[i] more difficult than if it were defined, and it certainly does not impact the soundness in cases where i is within bounds.

That's because you know the surface area of what's defined and what isn't already. If the behavior for a[i] were undefined for all cases of a[i], then you wouldn't be using a[i] at all because you'd have no idea what to expect about its behavior.

> I agree that undefined behavior is a problem, but it is not necessarily "worse" than other problems

You seem to be making this argument on the basis of taking for granted that you know something about what is defined already. Here's how to know that undefined behavior is worse. Say I asked you to write a program for your own pacemaker in a language where _all behavior_ is undefined. What do you do? It will be impossible to avoid killing yourself except entirely by accident, unless you resort to external validation methods.

The assurances that are possible in things you're describing are predicated on having some known a priori model for the domain of what is defined and what isn't, and the various certification/qualification methods required to use certain technologies & tools in domains where these things tend to matter focus on keeping engineers inside the bounds of what's defined and reducing the scope of what is undefined for a given configuration in-use.

> The whole point is to have evidence of turning unknowns into knowns for a defined set of deployment constraints.

Maybe, but undefined behavior still doesn't kill soundness.

> That's because you know the surface area of what's defined and what isn't already.

Sure, but in every programming language most of what you do is defined, even in C.

> Say I asked you to write a program for your own pacemaker in a language where _all behavior_ is undefined. What do you do? It will be impossible to avoid killing yourself except entirely by accident, unless you resort to external validation methods.

It's impossible to write any program in a language where all behavior is undefined. Such a language, by definition, has no semantics, and so no notion of a program. In fact, a language with no semantics of any kind is not a language at all.

> The assurances that are possible in things you're describing are predicated on having some known a priori model for the domain of what is defined and what isn't,

This is true for all programming languages.

> It's impossible to write any program in a language where all behavior is undefined. Such a language, by definition, has no semantics, and so no notion of a program. In fact, a language with no semantics of any kind is not a language at all.

So, it's necessary to remove a sufficient amount of undefined behavior before something is even usable in a coherent way? Which is another way of saying, you have to have defined enough behavior to be able to even get to the point of knowing whether or not the programmer is the one responsible for the "bug".

Undefined behavior seems to be necessarily worse than programmer error, since to be able to determine the latter you have to have removed some part of the former.

:shrug:, going to get back to work.

Undefined behavior means that certain expressions, like 1/0 in arithemtic, have no meaning; i.e. they are grammatically correct but nonsensical. For something to be a language, it is necessary for it to be able to state things that do have a meaning. But if some of its sentences have no meaning, it does not necessarily impact those that do. You don't need to "remove" anything. By default, sentences people say have meanings but not all of them do. To understand the sentence "I like pizza" you don't need to "remove" any undefinedness, just as you don't need to "remove" undefinedness to determine 2 + 3 = 5 even though some arithmetical sentences are meaningless, like 1/0 < 5.

It's like asking which is "worse", saying "England is a country in Africa" (false) or "Love ate a circle" (meaningless)? Both are "bad" in their own way.

But undefined behavior can certainly be inconvenient, because it is insufficient to determine whether a sentence is "well-formed", i.e. grammatically correct, in order for it to be meaningful, as some grammatically correct sentences are nonsensical. But it's certainly not catastrophic, because mathematics has a lot of undefined sentences, and we still use it successfully.

Having read this entire exchange I can say with absolute certainty that I did not understand it at all. I did however enjoy it very much.

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

Do linear and/or dependent types change this statement?

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.

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.

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?

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

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.

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

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

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

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.

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