5 ms·

One thing that's important to emphasise: sound safety, i.e. using a safe language, is no one's goal; rather, it is a means to end. What people want is correct p

by pron 6y ago

One thing that's important to emphasise: sound safety, i.e. using a safe language, is no one's goal; rather, it is a means to end. What people want is correct programs. The question is, then, does a language help write correct programs? Ensuring safety from important classes of bugs with sound guarantees is one way to help write correct programs, and both Zig and Rust use it; ensuring safety from from important classes of bugs with sound guarantees based on runtime checks is another way, and both Zig and Rust do it, too; a simple language that's easy to understand and analyse is another very important way to help write correct programs, and both Zig and Rust try to be simpler than their predecessors; making it easy to write tests and run them frequently is another way to get more correct programs that both languages try to employ. Both languages drastically differ in the use of those techniques from either C or C++ because they are both languages that put a very strong emphasise writing correct programs, but they also differ a lot from each other in how they balance those techniques. It is impossible to tell without careful empirical research which helps write correct programs more than the other, and it is also possible that different people find it easier to write correct programs in either Zig or Rust. Rust certainly provides stronger guarantees that prevent temporal memory bugs than Zig, so let's assume Rust programs will contain zero, and a Zig program will contain more than zero but much less than C or C++. But that delta is insufficient to determine that Rust's balance of techniques reduces more bugs overall. Also, Zig already has decent checks for use-after-free, and they'll get better, and not having uninitialised memory is also very easy to do (and verify) in Zig, despite there not being any checks. Even if, like other runtime checks, it is turned off in production, it still helps catch errors in that category.

HourglassFR 6y ago
I've seen you make that argument a few times on Zig related discutions but I'm not sure I buy it. It essentially boils down to: simpler language => easier to reason about and build tools for => less bugs. While the thought as merits, the empirical evidence we have indicates that yes it is possible to achieve good software with faulty languages with strong rules and tooling but it is certainly not as straightforward as you make it seem. In the end though, for the Zig case I agree that the jury is still out. But if I was a betting man, my money would not be on it, even though personnaly prefer Zig.
- mtzet 6y ago
  You're also forgetting: simpler language/explicit code => faster build times. Zero-cost abstractions are only zero-cost in optimized builds and and complex optimization isn't free. Whether static checking vs faster iteration time is more important depends entirely on the context, but rust isn't going to help you when you accidentally did front-face culling instead of back-face culling.
  - pjmlp 6y ago
    Eiffel, Delphi, Nim and D have very fast build times, and are all relatively complex. Even C++ can have relatively fast build times, depending on how everything is structured, and the use of binary libraries. It is a matter of tooling, as an anecdote all my UWP C++ applications compile faster than most of my Rust experiments.
- pron 6y ago
  > but it is certainly not as straightforward as you make it seem. I never claimed it is straightforward; it is anything but. As a practitioner and advocate of formal methods and verification, I've been following research in software correctness for many years (and have written much about it, e.g. https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity), I've come to realise how complex the problem is, and there's more we don't know than we know, and even the things we know are problems, we don't know what the best solution is, because often solutions carry with them more problems. Nonetheless, there are certain principles. We know that we can eliminate certain bugs with compile time guarantees; we also know that code reviews catch many (many!) bugs, and so making them easier helps. But what if these two are in opposition? It's not easy to tell which wins in which circumstances. > In the end though, for the Zig case I agree that the jury is still out. True, but the jury is still out on Rust, too. In fact, for most languages. However, there is no clear argument that we should assume, a priori, that Rust results in more correct programs than Zig. Many such arguments in the past have failed to yield positive empirical results (e.g. https://youtu.be/ePCpq0AMyVk https://youtu.be/ePCpq0AMyVk). In fact, given empirical research, the safest bet is to assume the null hypothesis -- that there is no difference. Out of an abundance of caution, I'll assume that languages whose designers place a strong emphasis on correctness might achieve it more easily than languages whose designers put no emphasis on it at all, but Zig and Rust are in the same category here. Both are designed with correctness as a primary goal. But as their design and means of achieving correctness is so different, I think it's impossible to make an educated guess as to which of them, if any, yields more correctness more easily. If we want some bottom line, it is this: software correctness is so complex, and solutions are often so non-obvious (i.e. many work in theory but not in practice), that we cannot say anything with certainty until we have actual empirical results, and even then we need to be careful not to be careful not to extrapolate from one study to other circumstances with different conditions (i.e. that TypeScript seems to have fewer bugs than JavaScript does not seem to extrapolate to the general claim that typing always reduces bugs compared to no typing in the same amount or at all, when other languages are concerned).
lmm 6y ago
> What people want is correct programs. At first order not even that; 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. 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.
- 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).
pjmlp 6y ago
From my point of view until Zig fixes the issues marked as none on the table, it adds very little value to existing alternatives. I can already use C and C++ to suffer that in production, use VC++ static analysers to mitigate them, while languages like Ada, D, Rust, Nim, Swift take care of them not happening at all.
- pron 6y ago
  Zig's safety is not at all like C's (or even C++'s), even with static analysers and sanitisers. It is core to the language through things like slices and nullability types. What Zig brings to the table is an extremely powerful and expressive, yet remarkably simple language that places as much emphasis on correctness as Rust (albeit in a radically different way).
  - Ar-Curunir 6y ago
    I don't think you can say that Zig is as correct as Rust given that memory-safety is not guaranteed by Zig (as evidenced by the article we're commenting on).
    - pron 6y ago
      Whether a language is "correct" is meaningless (hopefully, most compilers/interpreters are reasonably correct); we're talking about which language makes it easier to write correct programs, and because both languages focus heavily on that goal yet take very different approaches to achieving it (the article only compares one), it is simply impossible to tell at this point which of those languages, if any, achieves that goal better than the other.
      - pjmlp 6y ago
        Except you are assuming that Zig will never change after 1.0 release. C17 is also quite different from K&R C, specially in what optimizers do with UB. The only way OS vendors have to fix issues that Zig also shares with C, C++ and Objective-C, as per the article, is to adopt hardware memory tagging, something already available on Solaris SPARC, Azure Sphere and iOS (yes PAC is a bit different), with ongoing work for ARM. So I really don't see the benefit, but lets see how Zig 1.0 actually looks like, and I might be wrong by then.

by pron 6y ago

HourglassFR 6y ago

I've seen you make that argument a few times on Zig related discutions but I'm not sure I buy it. It essentially boils down to: simpler language => easier to reason about and build tools for => less bugs. While the thought as merits, the empirical evidence we have indicates that yes it is possible to achieve good software with faulty languages with strong rules and tooling but it is certainly not as straightforward as you make it seem. In the end though, for the Zig case I agree that the jury is still out. But if I was a betting man, my money would not be on it, even though personnaly prefer Zig.

mtzet 6y ago
You're also forgetting: simpler language/explicit code => faster build times. Zero-cost abstractions are only zero-cost in optimized builds and and complex optimization isn't free. Whether static checking vs faster iteration time is more important depends entirely on the context, but rust isn't going to help you when you accidentally did front-face culling instead of back-face culling.
- pjmlp 6y ago
  Eiffel, Delphi, Nim and D have very fast build times, and are all relatively complex. Even C++ can have relatively fast build times, depending on how everything is structured, and the use of binary libraries. It is a matter of tooling, as an anecdote all my UWP C++ applications compile faster than most of my Rust experiments.
pron 6y ago
> but it is certainly not as straightforward as you make it seem. I never claimed it is straightforward; it is anything but. As a practitioner and advocate of formal methods and verification, I've been following research in software correctness for many years (and have written much about it, e.g. https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity), I've come to realise how complex the problem is, and there's more we don't know than we know, and even the things we know are problems, we don't know what the best solution is, because often solutions carry with them more problems. Nonetheless, there are certain principles. We know that we can eliminate certain bugs with compile time guarantees; we also know that code reviews catch many (many!) bugs, and so making them easier helps. But what if these two are in opposition? It's not easy to tell which wins in which circumstances. > In the end though, for the Zig case I agree that the jury is still out. True, but the jury is still out on Rust, too. In fact, for most languages. However, there is no clear argument that we should assume, a priori, that Rust results in more correct programs than Zig. Many such arguments in the past have failed to yield positive empirical results (e.g. https://youtu.be/ePCpq0AMyVk https://youtu.be/ePCpq0AMyVk). In fact, given empirical research, the safest bet is to assume the null hypothesis -- that there is no difference. Out of an abundance of caution, I'll assume that languages whose designers place a strong emphasis on correctness might achieve it more easily than languages whose designers put no emphasis on it at all, but Zig and Rust are in the same category here. Both are designed with correctness as a primary goal. But as their design and means of achieving correctness is so different, I think it's impossible to make an educated guess as to which of them, if any, yields more correctness more easily. If we want some bottom line, it is this: software correctness is so complex, and solutions are often so non-obvious (i.e. many work in theory but not in practice), that we cannot say anything with certainty until we have actual empirical results, and even then we need to be careful not to be careful not to extrapolate from one study to other circumstances with different conditions (i.e. that TypeScript seems to have fewer bugs than JavaScript does not seem to extrapolate to the general claim that typing always reduces bugs compared to no typing in the same amount or at all, when other languages are concerned).

lmm 6y ago

> What people want is correct programs. At first order not even that; 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. 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.

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

pjmlp 6y ago

From my point of view until Zig fixes the issues marked as none on the table, it adds very little value to existing alternatives. I can already use C and C++ to suffer that in production, use VC++ static analysers to mitigate them, while languages like Ada, D, Rust, Nim, Swift take care of them not happening at all.

pron 6y ago
Zig's safety is not at all like C's (or even C++'s), even with static analysers and sanitisers. It is core to the language through things like slices and nullability types. What Zig brings to the table is an extremely powerful and expressive, yet remarkably simple language that places as much emphasis on correctness as Rust (albeit in a radically different way).
- Ar-Curunir 6y ago
  I don't think you can say that Zig is as correct as Rust given that memory-safety is not guaranteed by Zig (as evidenced by the article we're commenting on).
  - pron 6y ago
    Whether a language is "correct" is meaningless (hopefully, most compilers/interpreters are reasonably correct); we're talking about which language makes it easier to write correct programs, and because both languages focus heavily on that goal yet take very different approaches to achieving it (the article only compares one), it is simply impossible to tell at this point which of those languages, if any, achieves that goal better than the other.
    - pjmlp 6y ago
      Except you are assuming that Zig will never change after 1.0 release. C17 is also quite different from K&R C, specially in what optimizers do with UB. The only way OS vendors have to fix issues that Zig also shares with C, C++ and Objective-C, as per the article, is to adopt hardware memory tagging, something already available on Solaris SPARC, Azure Sphere and iOS (yes PAC is a bit different), with ongoing work for ARM. So I really don't see the benefit, but lets see how Zig 1.0 actually looks like, and I might be wrong by then.