---
This is my main issue with Rust. It doesn't seem to really solve the right problem. I feel like it solves the easy problems that I already know how to solve easily, but as soon as I get to something that really, truly feels like I want it, the best solution is unsafe.
A complicated circular linked data structure is exactly where I want the language to be screaming at me if I make a silly error. But Rust doesn't even consider memory leaks to be errors...
But I'm not happy trusting that dependencies aren't using unsafe code, and I'm not happy claiming that Rust ensures safety, when it ensures safety only if you assume that unsafe blocks aren't unsafe.
The problem is that you can't check unsafe blocks locally. Checking that each individual unsafe block doesn't have undefined behaviour requires checking the entire programme.
It's better than nothing, without a doubt, but it isn't safe.
For nontrivial libraries that use a lot of unsafe, it really is very difficult to know that all the uses of unsafe don't interact in some way to create unsafety. The scoped lock that had a problem in Rust 1.0 (or just before it?) is an example.
You can force callers to maintain your invariants in C++ too, simply by using some basic safety. Yes people can still do things that are obviously visually unsafe in code and undefined, but that's not a serious issue.
I still think Rust is better here. Don't get me wrong. But it's very hyped as 'safe and fast' when it just isn't safe.
The problems with engineering solutions that approach something close to the end of the spectrum of perfection, is that it gets undo criticism for not being perfect-enough. Rust is hopefully a stepping stone along path towards more correct, less error prone computation. Lets not throw the baby out with the bathwater.
Almost all of the code I write just uses prebuilt data structures (other then structs to group things) and when writing this code I find the safety measures that rust provides very convenient because I don't have to worry about these things such as lifetimes. It is nice knowing that the compiler will let me know if I make an error.
However yes, it doesn't solve the hard probem of complex circular structures. I don't see this as a major issue because when I am writing these I am carefully thinking about the strucutre anyways. So yes, while it would be nice to have these verified as well I wouldn't want take the tradeoff if it made the language much more complex.
The idea that Rust would be no better than C/C++ because of the latter parts doesn't make much sense. This kind of work is unusual for most programming. To say that other programming work is easy does not seem to bear out in practice.
And as has been becoming clear in this thread, if you're inventing new data structures, the odds are you overlooked an already existing better alternative.
My point is that the whole point of Rust is supposedly that it
>is a systems programming language that runs blazingly fast, prevents segfaults, and guarantees thread safety.
except that when you look at any of the examples of code that really would benefit from the compiler's help, the compiler just throws its hands in the air and goes 'it's all up to you now'.
The problem is that Rust doesn't let you make a single assumption and let the compiler prove the safety of the code using that assumption. It just has a valve that you can hit that removes all guarantees.
If you could say 'this code is safe assuming that this FFI function doesn't exhibit undefined behaviour, please check that for me' or write a proof that says 'this actually is safe, because this pointer can only ever point into this valid memory or this valid memory, and this is why' then the compiler would still be useful.
Whether 'this work' (which is not just creating data structures, but anything that the compiler doesn't understand, which is much broader than just creating data structures) is unusual or not, IMO the whole appeal of Rust is that it makes doing that work easy. But it doesn't.
Rust just doesn't seem worth it, doesn't seem worth rewriting whole ecosystems of code. It doesn't give any actual safety.
This seems to be the point of disagreement here, and I think evidence clearly shows that you are wrong. Sure, Rust doesn't help you when writing the implementation of e.g. circular data structures. But what it does do is provide, far beyond C or C++, the tools for the author of that data structure to enforce that it's used correctly.
And as mentioned upthread, most memory/concurrency (especially concurrency) bugs are not in the implementations of these structures, but in their use. So Rust is a fantastic win here, empirically speaking. Look at the rate of memory safety bugs in Rust programs vs C++ programs- Ripgrep vs grep, Servo/Quantum vs Firefox, etc.
* Most developers are not writing data structures, so optimizing for that seems unnecessary.
* There is work and research going into verifying unsafe code
* I think historically we can see that most memory safety vulnerabilities are not going to be in some lower level data structure, which is well encapsulated and likely already built by someone else, but in the use of that data structure. In particular - sharing references and also invalidating data safely without leaving references to that data. Rust helps you here, and this seems like the far better target.
* Even if your rust code uses unsafe, you still have benefits - you know where to audit for unsafety, you know where to pay extra close attention, and you can still write a large portion of your code in safe rust.
Edit: or try something like Idris. But I think you're asking too much of today's rustc.
The simple way to do that would be to allocate an array, and use indices into the array rather than pointers/references.
Doing it with pointers isn't so much harder in Rust than C as it is that Rust is making you deal with how hard it is to get this right, whereas in C the compiler is happy to let you think it's easy while you accidentally shoot yourself in the foot.
If you want the Rust compiler to accept your mistakes, you can always wrap it in an unsafe block ;)
The thing that makes this hard in rust is destructors. If there's a cycle between A and B, and you destruct A first, then B, then B's destructor would see a dangling reference to A. And vice versa if you destruct B first.
But I don't need destructors, or at least ones that can see these references, so it's frustrating.
It's still "hard to get right" in that at any time nothing is stopping you from violating any of the assumptions that make this "easy". It's never easy to write a solution that's "guaranteed to be safe" in C, but that's what you're trying to do by writing such a solution in Rust. To give but one example, nothing in C will stop your nodes from containing some resources which needs to be manually destructed and which get leaked when the stack frame is reclaimed.
Rust is going to require you to make those assumptions explicit, so that it can enforce them -- in this case, you need to explicitly restrict your solution to dealing with Copy types, which by construction don't implement Drop, and therefore have no destructors.
But at the end of the day, if all you want to do is swear to the compiler that you know what you're doing and you promise to not be stupid, wrap it in an unsafe and get C-style consequences if you got things wrong. You get C-Style easiness only by explicitly abandoning the attempt at guaranteeing safety for every type and scenario your solution could be used with.
If you bound it so that it only accepts Copy types, then you can know there are no destructors.
I've done that in code for a collision detection engine. The object descriptions for convex polyhedra have lists of faces, lists of edges, and lists of vertices, all referencing each other. The original implementation (I-Collide) actually used lists for them. When I re-implemented that in C++, I used arrays with indices for each of those. When you're done with a polyhedron, all those structures, which are owned by the Polyhedron object, go away more or less simultaneously.
Using unsafe blocks throws all that away.
Regarding everything being destructed at once: that’s called an arena, and there are crates for it:
Thats such a great name :)
What you do is you put all of your tree nodes in a big Vec<Node> and instead of referring to children and parents via pointers, you do so via indices. It's less convenient because you have to pass around a reference to your "arena" everywhere (the Vec or a slice of it), and it incurs bounds checks (pretty cheap though). But, it solves the problem in a way that is guaranteed safe.
However, you must have interior mutability (achieved using Cell types), because otherwise you can't mutate the parent nodes to add links to child nodes.
Check the typed arena crate in crates.io and the Cell type in the standard library.
It'd likely be the other way, that is, you'd put a RefCell inside of an Rc/Weak.
> it doesn't look like refcell works well with traits
It should; I bet you had problems since you did it the other way around.
> I'm a bit frustrated because this is so easy in C.
You could do it the same way as you do it in C, if you're willing to resort to `unsafe`.
FWIW, Rust sort of changes the equation for what's easy here; thread-safe concurrency? Simple! Data structures? Hard! C is the other way around. So feeling a bit frustrated is normal; your C skills won't carry over, but it feels like they should.
> I am imagining a special way to construct cyclical structures where everything inside would have the same lifetime and be destructed at once
This sounds like an arena to me, which is another option, for sure.
If you post to https://users.rust-lang.org/, someone might be willing to whip up an example, or if you post your in-progress stuff, someone might be able to fix it for you.
https://crates.io/crates/petgraph might also just already have what you need, maybe.
It's a good point that maybe I should just have the right expectations here, and expect data structures to be hard in rust.
I looked around a bit and it looks like these thing are quite challenging in haskell as well.
$ ghci
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> let ones = 1 : ones
Prelude> take 50 ones
[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Obviously, this is a trivial example, you can do much more interesting things with mutually recursive bindings.
let cycle = "cycle " ++ cycleUsing strict data types, I think you agree that cycles can not be created. Non strict data structures I agree can be seen as cyclic, but I prefer seeing them as infinite.
RefCells seem to add unnecessary redundancy here. You'll take a hit for runtime borrow for every pointer chase up the tree. If walking from a leaf to the root is important, you don't want to add an extra compare/branch/set to every pointer chase. Turns a single memory read into a branch, a write, and two reads. Probably about 5x slower at least.
The answer isn't generics, Coq, or some fancy type system nobody will understand or use properly. There are only a few inherent trouble spots in pure Rust code safety. The big two are:
- Partially initialized arrays. "Vec" has to be unsafe because growing an array involves uninitialized slots. You just need a way to say "this array is initialized from 0..N only", where N is in a data structure associated with the array. Then you need an operation that says "initialize entry N+1 and update the count". That's all it takes.
"Map" could be implemented on top of "Vec", instead of using unsafe code. It would be worth trying this and seeing what the performance penalty is. That may be a premature optimization.
- Backpointers. Backpointers have an easily checked invariant relationship with the forward pointer that owns their containing object, but there's no way to tell the language that something is a backpointer.
The solution is a formal semantics for unsafe Rust, so that programmers can prove that their unsafe Rust code is safe to use by whatever means they prefer. (Mine would be by hand.)
---
Reply to dmix:
A formal semantics doesn't have to be particularly fancy, although in Rust's case, it will in most likelihood not be straightforward either.
The partially initialized array thing is an issue of expressive power. You can't talk about that in Rust yet. This is a classic issue. The three big headaches in C around memory safety are "how big is it", "who owns it", and "who locks it". The language lacks the syntax to even talk about those issues. Rust can talk about those, which is a huge step forward.
Before you can even consider verifying something, you have to be able to talk about it in some formal language. Preferably the one you're programming in. Having to do formal specifications in a separate language is a huge headache. Been there, done that.
There are a few standard trouble spots. I've listed two of them. Most other unsafe code comes from
1) Foreign functions, which can be expected to decline over time as more libraries are implemented in Rust. (How's SSL/TLS in Rust coming along?)
2) "Optimization", which may be premature. This usually consists of bypassing subscript checks. I'd rather have the subscript checks on all the time, and see effort put into hoisting subscript checks out inner loops. (Subscript checks that aren't in inner loops usually aren't significant overhead items.)
3) replicating C/C++ code in Rust. (An early attempt was a transliteration of Doom into Rust, with lots of pointer arithmetic.)
Remember, it can blow at any seam. It only takes one buffer overflow to allow an exploit.
I'd personally be excited too see a modern language implement this. I saw the potential for this type of verification in my (hobbyist) dabbling with Haskell. Which subsequently inspired me to relearn math, including a great book on proofs recommended on HN which really changed the way I viewed/approached math.
The use-case analogies for formal verification can probably best be drawn from automated testing and TDD. Which is another 'optional' part of programming with varying degrees of usage - although with a lower barrier to entry.
Types/proofs seem to have a positive influence on the 'best practice' part as well, as it promotes a programming style which force you to really consider the implementations you're coding. Very similar to testing.
At the moment formal proofs tools today seems to me like a rabbit hole with questionable practical ROI so I've been hesitant to try out the current state-of-the-art.
Assuming it does get built in to the language, even if it doesn't get used by the user they will likely benefit just by being able to build on layers beneath that were proven in the standard/popular libraries. I felt a similar feeling of assurance when building on top of well-typed Haskell libraries.
But Pascal was a small language. Getting this into today's bloated languages is tough. Back then, we looked at Ada, sized the project, and realized it was comparable to building an optimizing compiler for the language.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
You sound like a very interesting person to buy a beer for, assuming you'd be patient enough for my questions :p, I'll check out the paper instead when I get the time.
> It's much easier to keep the verification statements correct if they're in the same file and the same language as the program.
Agreed. Hell even using Dialyzer in Erlang/Elixir for static type checking (which I make the effort to do often in my daily side project hacking) just doesn't feel right, even though it's still appended to function definitions in the original files.
This is one of those things that need to be a core part of the language design IMO, not just a tool built on top - 3rd party, by the core team, or otherwise. But, that said, tooling can still be superior compared to the complete absence of it.
Maybe you can answer a question I've been struggling to find the answer to via Google. Do you know the name of this popular older language/tool used by to Microsoft for doing formal verification? For c/c++ style code. It sounds like tkk or something similar? I can't seem to find it.
My other question I'd ask is if you think the testing analogy applies here as I mentioned in my comment above or do you see it as an entirely different paradigm? Basically changing how you program rather than adding on a tool/skillset.
Sure, but it doesn't have to be a programming language.
> Preferably the one you're programming in.
Who says so? Programming languages (justifiedly) optimize for the ability to express computation, not the ability to express proof.
In spite of Curry-Howard, there exist important differences between proofs and programs:
(0) Proofs are primarily for humans to understand. Programs are primarily for computers to execute.
(1) Proofs are sometimes allowed to be non-constructive. Even when they aren't, an easily understandable proof beats one that corresponds to an efficient program.
(2) Allowing non-terminating programs is actually a good thing: it allows for proofs of correctness that use techniques not anticipated by the language designer. OTOH, if your logic lets you prove a contradiction, it's the end of the world (for your logic).
defined(arrayname, lowbound, highbound)
defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1)
Think of proof support as being an extension to optimization of assertions. Most assertions in programs can be proven easily with an automated prover. Users need never see those proofs. Some will be hard and require more proof support.
And runtime checks help because...?
> But you'd rather prove it once so the run-time checks are unnecessary.
No. I'd rather prove it to rule out the program being wrong. The runtime check is totally besides the point.
> With a few simple theorems, such as (...)
I think you mean “proposition”. It's not a theorem until it has been proven.
> Think of proof support as being an extension to optimization of assertions.
I never use runtime-checked assertions, so I never need to optimize them away.
> Users need never see those proofs.
But, you see, I want to see the proofs. How am I supposed to maintain a program I don't understand?
defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1)
(PROVE-LEMMA arraytrue-extend-upward-rule (REWRITE)
(IMPLIES (AND (EQUAL (arraytrue A I J) T)
(EQUAL (alltrue (selecta A (ADD1 J))) T))
(EQUAL (arraytrue A I (ADD1 J)) T)))
Name the conjecture *1.
We will try to prove it by induction. There are three plausible (AND (IMPLIES (LESSP J I) (p A I J))
(IMPLIES (AND (NOT (LESSP J I))
(p A (ADD1 I) J))
(p A I J))).
Case 3. (IMPLIES (AND (LESSP J I)
(ARRAYTRUE A I J)
(EQUAL (ALLTRUE (SELECTA A (ADD1 J)))
T))
(ARRAYTRUE A I (ADD1 J))),
...
That finishes the proof of *1. Q.E.D.
"arraytrue" is defined recursively:
(DEFN arraytrue (A I J)
(IF (LESSP J I) T -- the null case is true
(AND (EQUAL (alltrue (selecta A I)) T) -- next element is true
(arraytrue A (ADD1 I) J))) -- and rest of array is alltrue
Sure. My point is just that a theorem is a proposition equipped with a proof. If the user just enters a proposition into the system, then they aren't entering a theorem. They're entering a proposition that the system can turn into a theorem.
> No. I'd rather prove it to rule out the program being wrong. The runtime check is totally besides the point.
That's the same thing. It's just a matter of it being automated.
> > Think of proof support as being an extension to optimization of assertions.
> I never use runtime-checked assertions, so I never need to optimize them away.
If you've ever used a language that uses bounds checked array access, you have. IIRC, you've used Rust some, so you've used bounds checked array access, except where Rust was able to prove that out of bounds access was impossible and elide the code that checks.
> > Users need never see those proofs.
> But, you see, I want to see the proofs. How am I supposed to maintain a program I don't understand?
There's a difference between need and ability. Just because it's stated you don't need to see something doesn't mean you can't. If you want to see a proof, you dig in and find it, or find where it's accepted canon that we don't need to reproduce (do we need proofs for integer addition? That seems of limited use to me, but maybe a formally proved as much as possible all the way to that level language has some interesting benefits).
Re-read what he said. He presented runtime checks as an acceptable but non-optimal scenario for performance reasons. My reply was that runtime checks don't prevent a wrong program from being wrong, and it's this wrongness itself that I consider unacceptable.
> IIRC, you've used Rust some, so you've used bounds checked array access, except where Rust was able to prove that out of bounds access was impossible and elide the code that checks.
Runtime bounds-checked array manipulation is literally the single thing I hate the most about the languages I like the most (ML and Rust). It introduces a control flow path that shouldn't be reachable in a correct program, and hence shouldn't exist. This is particularly painful because beautiful array-manipulating algorithms have existed since, like, forever, yet in 2017 I still can't express them elegantly.
> If you want to see a proof, you dig in and find it, or find where it's accepted canon that we don't need to reproduce (do we need proofs for integer addition)?
I don't need to rebuild arithmetic from scratch again, because I've already done it at some point in time, and once is enough as long as you understand the process.
On the other hand, when I'm first confronted with an already existing program, I don't understand why the program is correct (if it is even correct in the first place), so I do have to set some time aside to properly study it.
How does that special hash marker work? What happens when something actually hashes to it? Just silently increment the hash?
Yes, but it's a single contiguous memory allocation. (It used to be three parallel vectors in a single allocation, with keys and values also kept separate to avoid padding between them, but experiments showed that had worse cache behavior.)
> How does that special hash marker work? What happens when something actually hashes to it? Just silently increment the hash?
Looking at the code, it always sets the most significant bit of every real hash value (since the least significant bits select the bucket, it makes no difference), and the marker has the most significant bit clear (in fact, all bits of the marker value are clear).
So in this case the code generated is idential to a nullable pointer.
Speaking of paradigms, although Rust definitely looks "imperative", the ownership system makes it bloody different. Try to implement a tree "as in C" using Haskell or Prolog and you will lose time and energy for a result that does not use the language to its fullest.
Sure. But that's true for every programming languages, at least in my experience.
Anyway, someone, somewhere will actually want/need that tree. And they'll run into the aforementioned problems.
https://github.com/stjepang/vec-arena/blob/master/examples/s...
I'm a bit frustrated because this is so easy in C. Is there any way this can be easier?
I am imagining a special way to construct cyclical structures where everything inside would have the same lifetime and be destructed at once. We may need to hide the references from destructors though, otherwise a destructor could see a dangling reference.