3 ms·

> what people want is programs that behave correctly (or correctly enough for their purposes, which may not be very correct at all) for their particular inputs

by pron 6y ago

> what people want is programs that behave correctly (or correctly enough for their purposes, which may not be very correct at all) for their particular inputs and execution environment. Ah, yes. This raises an interesting philosophical question with real ramifications for software quality assurance: is a bug in the algorithm that never manifests in the system really a bug? Something like that happened in two well-used pieces of code: There was a bug in the TimSort algorithm used in both Java and Python, whose probability of actual failure is similar to the probability of failure due to a bit flip caused by cosmic rays. Because hardware can only be correct with probability, no running system can be soundly verified, i.e. with certainty, anyway, so while the correctness of algorithms can be absolute, the correctness of system cannot. And since soundness has a big cost in verification, many in software correctness research now focus on unsound techniques that are cheaper. > Conversely those of us who want the industry to advance the state of the art generally don't want to just produce correct programs at a particular point in time, but programs whose correctness can be easily maintained even as implementations and requirements change. More than that, we want to produce libraries and frameworks that will lead as-yet-unknown programs to be correct. True, but that is not a winning argument for soundness. The cost of soundness manifests even at maintenance. It's therefore an equally strong argument that a language that compiles quickly and more easily allows running, say, concolic tests, mutation tests etc., serves that goal, too.

pron 6y ago
P.S. A language that makes code reviews easier also works toward that goal of maintaining program correctness over time. The point is, there are many different paths to correctness, all of them state-of-the-art yet are often in conflict with one another, and we don't have any mechanism other than empirical research to compare them. For example, is it beneficial to increase soundness at the expense of making code reviews harder? Not only do we not have an answer to that question, it is likely that there is no general answer (I say it's likely because whatever empirical research we do have shows messy results with large variance).
- dnautics 6y ago
  > A language that makes code reviews easier So much this. And also keep in mind the way that we typically do code reviews, we typically are looking at github diffs. So if you are in a situation where changing code is ill-composable, for example, if something looks safe in place A and something looks safe in place B but when you put them together it's not unsafe... Then you could be in deep trouble with the async way that we do reviews.

by pron 6y ago

pron 6y ago

P.S. A language that makes code reviews easier also works toward that goal of maintaining program correctness over time. The point is, there are many different paths to correctness, all of them state-of-the-art yet are often in conflict with one another, and we don't have any mechanism other than empirical research to compare them. For example, is it beneficial to increase soundness at the expense of making code reviews harder? Not only do we not have an answer to that question, it is likely that there is no general answer (I say it's likely because whatever empirical research we do have shows messy results with large variance).

dnautics 6y ago
> A language that makes code reviews easier So much this. And also keep in mind the way that we typically do code reviews, we typically are looking at github diffs. So if you are in a situation where changing code is ill-composable, for example, if something looks safe in place A and something looks safe in place B but when you put them together it's not unsafe... Then you could be in deep trouble with the async way that we do reviews.