To this I have two questions: - What kind of macros? (C-style or Lisp style?) - How do you check for memory safety? Rust gives you ownership guarantees at compile time. Maybe that's what makes it much slower to check
-
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
-
Think of a multithreaded system. How do you cooperate between threads? How do you share memory? That is not easy, and more often than not you end up pulling the rug from under some other thread's feet.
-
Rust forces you to not do that: only one thread can examine memory that's being modified at one particular time. This is their restriction on aliasing.
-
But how is this useful outside of a multithreaded scope? Well... Think of a library that you're building. Maybe a simulation, given your background on videogames. The more distant two pieces of code are, the least conscious you are of the influence one has over the other.
- 8 more replies
New conversation -
-
-
Is "general correctness" even achievable by the means of a language? If I understand it correctly, Jai is about reducing friction to a minimum, thus allowing to focus more on the problems at hand. It's a step towards achieving correctness, but so is memory safety etc., isn't it?
-
Yep! Somewhat of a holy grail is achieving general correctness with good enough ergonomics and performance to be used in general programming. Agda, Coq and Idris allow you to achieve general correctness, but the ergonomics are still lacking and the performance is still a WIP
-
There is hope in the performance front: the more information you give a compiler, the more it can reduce the scope of your program and optimize it. Therefore a smart enough compiler should be able to give you C-level performance given a language that's expressive enough.
-
In the ergonomics, I feel we are still ways off. We'll probably need incredibly good tooling, because expressing yourself in those languages is very very hard.
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.