Comment by pron
1 day ago
> You messed up writing safe to unsafe interface (and forgot to sanitize your binary afterwards).
That is the definition of a language not being memory-safe. Memory-safety in the language means a guarantee that the resulting program is memory safe, and that you could not mess it up even if you tried.
Taking that to the extreme, it's like saying that a C program isn't memory safe only if you mess up and have UB in your program, something that C program must not have. But C is not a memory safe language precisely because the language doesn't guarantee that. My point is that there's a spectrum here, the goal isn't memory-safety in the language but in the resulting program, and that is usually achieved by some combination of sound guarantees in the language and some care in the code. Of course, languages differ in that balance.
> That is the definition of a language not being memory-safe. Memory-safety in the language means a guarantee that the resulting program is memory safe, and that you could not mess it up even if you tried.
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.
> But C is not a memory safe language precisely because the language doesn't guarantee that.
C isn't memory safe because it has 212 different ways to cause memory unsafety. And only offers externals runtime tools to deal with it.
I mean Rust will never be perfect due to Rice Theorem. It doesn't have to be either. It's at close to ideal as you can get, without mandating that programmers are perfect (no language errors) or that everything be written in safe Rust (no C bindings).
This is a well known Nirvana fallacy. E.g. If a cure doesn't cure fatal disease in 100% of cases why not let disease take its course?
> 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.
5 replies →