Jon's language and Rust are very different tools. If you ask me, I'd guess the complexity of compiling Jai must be between O(n) and O(n log^k n). That's how fast you can get if you make it a top priority ^^ It's all about tradeoffs, at the end of the day :)
-
I think that correctness is definitely a priority. Have you seen Ralf Jung's working group research of the `unsafe` uses within the stdlib and the compiler? Unless we're talking about a different form of correctness. I'm mostly talking about avoiding UB and vulnerabilities.
Then I think you are using the word "correctness" too loosely and charitably (as I think the entire Rust community does). Avoiding UB and vulnerabilities is good, but correctness means the program doesn't have bugs.
-
-
Ah yes, you're using a stricter form of correctness. Let's picture the space of bugs that will probably appear in a program. To me (loose correctness), ensuring correctness is proving that there's a region in that space that you'll never visit. Perfect correctness (yours) is (1/2
-
great, but afaik is only provable using very much cutting edge technology like Agda, Coq or Idris. Without at least fully dependent types you aren't able to prove that your program has absolutely no bugs. Maybe in 20 years or so that tech will be ergonomic enough for daily use :)
-
I am not talking about absolutely no bugs. I am just saying, an approach that is about general correctness, would look very different from an approach that is about memory safety + resource ownership.
-
It's fine, I think it's good that Rust is researching how to do a good job with memory safety + resource ownership without being a managed language. I just wish they would be clearer about what they are doing, and over-promise less.
-
How are they over-promising? (Honest question, I'd like to know your POV)
-
It's just distorted rhetoric. Almost none of the bugs we see are memory safety problems or resource deallocation problems. So the amount by which Rust would reduce our bug load is pretty small. So I don't think it can claim that it addresses correctness.
-
There is value in having more confidence that your program is memory-safe, if you are concerned about attackers. (But I also think we should just redesign our operating systems so we are less worried about attackers).
-
I think you're underestimating the influence of memory safety. In particular, more than avoiding vulnerabilities, it's avoiding aliasing: every bit has a clear owner. The compiler forces you to do that. And that is incredibly helpful. Lemme try to explain what I meanx
- 11 more replies
New conversation -
-
-
And "avoiding UB" is not really helpful if avoiding means trading it off for things that are technically not UB, but are still bugs.
-
That sounds scary, but where does that happen? I can't think of an example atm.
-
I think this is a good example of what Jon is talking about:https://www.youtube.com/watch?v=4t1K66dMhWk …
-
I got into a big discussion on Twitter after this with a relatively prominent member of the Rust community (since deleted since my tweets auto-delete) and he basically said, yeah, it is about memory safety, not about correctness per se. I forget who it was.
-
Hmm. That makes sense. Maybe what they're trying to say is that Rust is a stepping stone for a future where memory safety is solved and we can focus on other correctness issues that are currently even harder since we have to also deal with memory unsafety.
-
And by stepping stone, I mean for a better language to be invented after the next 10-20 years
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.