Comment by pron
1 day ago
> By your definition no language ever would be deemed safe. Even Java/C# has to interface with C. Or you have to write bindings for C libs/ kernel calls.
That's correct. My point is that even if we talk about memory safety only, languages are on a spectrum (e.g. Java programs don't need to use unsafe code as much as Rust programs), and there's always some situations where we don't rely on sound guarantees. In practice, we call languages that easily demarcate their unsafe code "safe languages".
> I mean Rust will never be perfect due to Rice Theorem.
That's nothing to do with Rice's theorem. A language that's completely, 100% memory-safe is not hard to do, but it will need to sacrifice some things that we don't want to sacrifice even for a 100% guarantee of memory safety.
> If a cure doesn't cure fatal disease in 100% of cases why not let disease take its course?
That's not a good analogy for software correctness. A better one would be that every cure has some side-effects. There are languages that, at least in principle, "cure" far, far more than Rust or even Java do, such as ATS or Idris. Why don't we always use them? Because it's hard! What we've gradually learned since the 70s (when a prevailing thought was that we'll have to use proofs to scale software) is that the cost of soundness can be high, and unsound methods (such as tests) are surprisingly effective in practice, and so "more sound guarantees" is not always the best answer. We now believe that for the best correctness per unit of effort we don't want no guarantees at all as in C, and we also don't want to guarantee everything as in ATS, but we're looking for some sweet spots in between. We haven't yet figured out what "the best" sweet spot is or, indeed, if there even is only one.
> That's correct. My point is that even if we talk about memory safety only, languages are on a spectrum
So are cars, there are cars that are a deathtrap, that send the steering wheel through your guts, and there are cars with seatbelts and airbags that won't save you from others or your own errors, but will minimize it. By your logic, I assume you're driving a Ford Pinto (Zig - has seatbelts but will explode at slightest touch).
You still wouldn't remove the seatbelts because they "chafe", or breaks because it's too much useless mass.
> In practice, we call languages that easily demarcate their unsafe code "safe languages".
That's not true. See Java, it doesn't demarcate unsafe code, you use the unsafe package. Granted, JNI looks about as weird
What in practice most people call safe languages are languages that preserve or have a high likelihood (looking at Go's memory model during data races) to preserve the spatial and temporal memory safety invariant, in absence of implementation errors.
> That's nothing to do with Rice's theorem
Wdym? The presumption is, you don't have a runtime, and you want safety. That means static checks. That means proving properties of your code, implying Rice's theorem.
> A language that's completely, *100% memory-safe is not hard to do.*
> My point is that even if we talk about memory safety only, languages are on a spectrum (e.g. Java programs don't need to use unsafe code as much as Rust programs), and there's always some situations where we don't rely on sound guarantees.
Huh? These two claims are in opposition. If it's easy (doable) to go 100% memory safe, then there should be a trivial way to always rely on memory guarantees. No need for a spectrum.
The spectrum exist because rather than writing OS in Ada, programmers collectively decided to bury their heads into C.
> That's not a good analogy for software correctness
It's not supposed to be a good analogy for software correctness, it was an example of Nirvana fallacy.
> There are languages that, at least in principle, "cure" far, far more than Rust or even Java do, such as ATS or Idris. Why don't we always use them?
Another Nirvana fallacy. On face value, this is an argument to move more to Rust, ATS, Ada and Idris, than it is to abandon them. Or for Rust to get linear types.
That said, in practice I understand these are proof languages with no ecosystem, that might reduce the likeliness of being used in production. But Rust has no such issues. It has a minor proof requirement (make sure your lifetimes are in agreement with the borrow model).
> Because it's hard!
If you avoid things that are hard, you'll never grow. If a programming language you learned didn't cause headaches, it's not a programming language, it's a dialect.
> See Java, it doesn't demarcate unsafe code, you use the unsafe package
The use of Unsafe in Java is demarcated, and besides, it is now being removed altogether, but we have more interesting things to talk about.
> That means static checks. That means proving properties of your code, implying Rice's theorem.
It doesn't. Rice's theorem talks about the undecidability of proving some arbitrary property of arbitrary programs, but given a property, one can construct a language in which it trivially holds for all programs in the language.
This is done by finding an inductive invariant -- one that is preserved by all program operations -- that implies the property. Let me give you an example. Due to Rice's theorem, it is undecidable whether or not the output of an arbitrary program that yields a number output is even. Nevertheless, it's easy to construct a language (even a Turing-complete one) where this property always holds. We find a stronger invariant -- all numbers in the program are even -- that can be easily made inductive. Indeed, even numbers are closed under addition, subtraction, and multiplication, while for every division operation we add a runtime check that panics if the result is odd (and, of course, the compiler rejects any literal that isn't even). And voila! Not every program that yields an even output can be written in this language, but every program in this language yields an even output.
To see that this is what Rust does with memory safety, note that while every program in safe Rust is memory-safe, not every memory-safe program can be written in safe Rust.
> If it's easy (doable) to go 100% memory safe, then there should be a trivial way to always rely on memory guarantees. No need for a spectrum.
The need for the spectrum arises because we want to sacrifice 100% memory-safety for other things, such as Java's ability to call C code.
> The spectrum exist because rather than writing OS in Ada, programmers collectively decided to bury their heads into C.
As someone who wrote safety-critical avionics software in Ada in the nineties, I can tell you that we had good reasons to largely abandon Ada.
> an example of Nirvana fallacy.
But it isn't because you assume that a language that makes more guarantees will always produce more correct programs per unit of effort, but we know that to be false.
From the vantage point of ATS and Idris, a language like Rust is almost indistinguishable from C. There are a few more properties it guarantees than C does, but ATS/Idris can be used to guarantee any program property. If what I said is a nirvana fallacy, then you must not use Rust and always use ATS, because it is much better on your definition of better. The reason we don't is that we know more sound guarantees are not always better, but we didn't always know that.
In the seventies, software correctness researchers (such as Tony Hoare) assumed that the only path to scaling software would be soundness (proofs, and even formal proofs). As time went on, we learnt that this belief was false from both sides: unsound methods proved surprisingly effective [1], and proofs proved costly to scale, to the point that they made achieving a required level of correctness more costly.
> If you avoid things that are hard, you'll never grow. If a programming language you learned didn't cause headaches, it's not a programming language, it's a dialect.
The problem is not in learning new languages. The problem is that more sound guarantees can sometimes reduce the cost of correctness and sometimes increase it.
Don't get me wrong: Soundness and proofs sometimes work very well, but we in the software correctness/formal methods world know that things are much more complicated than "more soundness more better".
You can read some of my writings on software correctness, after a couple of decades working with formal methods here: https://pron.github.io
[1]: https://6826.csail.mit.edu/2020/papers/noproof.pdf
> The use of Unsafe in Java is demarcated, and besides, it is now being removed altogether, but we have more interesting things to talk about.
If you call importing a package and using it demarcated, I have a bridge and some fog underneath to sell you.
> This is done by finding an inductive invariant -- one that is preserved by all program operations -- that implies the property.
This is a strawman fallacy, we're not talking purely theoreticals. Just because you can build a model of Empire state building from Legos doesn't mean that it will work for the real thing. Your Even Theorem Prover can't write 100 beers on the wall. Or even output Hello <name> for arbitrary name.
Rust, however, can maintain invariants and be expressive enough because it relies on outside the computer assistance (aka unsafe blocks).
> As someone who wrote safety-critical avionics software in Ada in the nineties, I can tell you that we had good reasons to largely abandon Ada.
As an outsider looking at commercial and military avionics failures (I can't be certain, but my guess is it seems cost-cutting on both hardware and software didn't quite pan out), I'm not sure that the right call was made.
> But it isn't because you assume that a language that makes more guarantees will always produce more correct programs per unit of effort, but we know that to be false.
Again, [citations needed]. Google mentioned they had little problem getting people to work with Rust. The onboarding time was around 3 months.
And statements that borrow checker is hard is no different, than saying, well, types are hard, generics are hard, covariance & contravariance are hard, indexes starting at 0 are hard, ones and zeroes are hard. To me, these are complaints of people that didn't run the gauntlet, and didn't build their "muscle memory" in programming.
> But it isn't because
You are using ATS and Idris as examples, and I agree, we should use them more. In fact, Rust extensions to generate proofs are amazing in my opinion, and both of those languages are remarkable. What they lack however is an ecosystem. Rust has that.
What does Zig give you? No ecosystem, no stability guarantees, and worse memory safety.
4 replies →