4 ms·

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

by 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.
- pron 7y ago
  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.

by pron 7y ago

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.

pron 7y ago
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.