> 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