Hacker News Reader

Comment by wireprotocol | Hacker News Reader

I've been having a little trouble using rust for a little project: I need a tree with uplinks (meaning there are cycles). I asked on IRC a couple times and I think what I need is a weak reference inside a refcell, but it's not very easy to make it work cleanly. For one thing, it doesn't look like refcell works well with traits (the nodes in the tree are traits, not plain structs).

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.

View on HN

Have you read "Learning Rust With Entirely Too Many Linked Lists"[1]? I think it will be quite helpful for these kind of situations. It walks you through all the possible tools in the language that is available to you, and at the end, if you just want to write it how you would in C, you could always do it "unsafely" with raw pointers (which is no worse than C).

---

[1] http://cglab.ca/~abeinges/blah/too-many-lists/book/

Beat me to this by six hours. Can vouch that the above link is quite helpful when learning Rust.

It's also really no better than C. Or at least no better than C++.

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...

Here have an upvote. Can someone else comment/refute this?

I don't really have a refutal, but more of a dismissal.

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.

Most of us write new, complex data-structures, that aren't part of the stdlib or a crate, like once a year, at most. Those are hard in Rust if they involve circular pointers. They're hard in C/C++ too, but in a different way (easier to write the code, harder to be sure it's correct).

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.

It doesn't matter that it's 'kind of unusual', even though I contend that it isn't. Even if, for the sake of argument, we assume that it is, that doesn't change my point.

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.

> examples of code that really would benefit from the compiler's help

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.

Sure...

* 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.

I don't know, ensuring memory safety at compile time and safe concurrency is a pretty big win for me over C, I know many people who claim that they can write/debug C programs to be memory safe, however the real world would respectfully disagree.

Rust doesn't ensure memory safety or safe concurrency. It ensures memory safety - including data race safety, just one part of safe concurrency - assuming you never use any unsafe code and that the standard library is free of bugs. I'm happy to assume the standard library is free of memory safety bugs, because you have to trust something.

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.

Unsafe blocks are infectious, that's true, but it's possible to write safe APIs that limit that infectiousness to a single module. For example, even though Vec's implementation is crazy unsafe, you don't have to audit all the uses of Vec in safe programs -- a local audit of the Vec code can prove what we need to prove. This is the biggest benefit of the lifetime system and the borrow checker, that when we write piles of unsafe code, we can force safe callers to maintain our invariants.

You can prove it, but you can also prove that a C++ programme has no memory safety bugs. And there are a lot of languages where you don't have to, where it's simply impossible to get memory safety bugs (assuming the runtime is 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.

AFAIK, verifying complex linked data structures is still an active research topic. For instance: https://cs.au.dk/~amoeller/papers/pale/pale.pdf

Edit: or try something like Idris. But I think you're asking too much of today's rustc.

If freedom from data and race conditions is the easily solved problems, I'll take it.

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.

> I am imagining a special way to construct cyclical structures where everything inside would have the same lifetime and be destructed at once.

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 ;)

While it may be simpler, it also removes any safety that rust adds. I'd imagine you'd get more mileage out of just using pointers and unsafe blocks liberally to get lifetime checking where you can.

It is still safer than c, as it will not allow any segfaults. The only thing that can happen is a runtime error but no memory corruption so it is more akin to say Java or Go

The context of this thread is unsafe, which can segfault.

You are describing the behavior of standard, safe rust code.

Using unsafe blocks throws all that away.

But in my example this is not hard to get right in C. The tree is constructed (on the stack would be fine), then used for a while without mutating it, then freed all at once.

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.

Since you want to use the C method, have you tried using raw pointers?

> But I don't need destructors, or at least ones that can see these references, so it's frustrating.

If you bound it so that it only accepts Copy types, then you can know there are no destructors.

Interesting. Then rust should not care about the destruction order, right?

For this purpose, no, I don't think. That said I might be missing something and maybe th compiler doesn't understand this, so I'm not saying it's a panacea in your case, just might be worth looking at.

The tree itself will need destructors to clean up allocations, and that's what's problematic here: if the tree is destroyed top down, the destructor of the children may access the parent which has already been invalidated, and similarly destroying bottom up risks the destructor of the parent accessing the children.

> But in my example this is not hard to get right in C. The tree is constructed (on the stack would be fine), then used for a while without mutating it, then freed all at once.

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.

Nothing stops you from leaking memory in Rust either, it is considered memory safe, see std::mem::forget. Rust only safes you from use-after-free and double-free.

And integer out of bounds, and (most) segfaults, and data races, etc

Notably integer overflow is NOT UB and is checked in debug builds.

Sorry, I should have said array OOB.

Yeah, it's all good!

The simple way to do that would be to allocate an array, and use indices into the array rather than pointers/references.

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.

Regarding traits: you can have Rc<Trait> (by casting from Rc<your concrete type>), but not RefCell<Trait>. The reason is that Rc is a pointer, so the size of Rc<Trait> can be constant regardless of the size of the type implementing the trait. But if you actually want a weak reference inside a refcell (as opposed to the other way around), RefCell<Weak<Trait>> should work fine. Also consider the Cell type, which has a more limited API than RefCell but zero overhead.

Regarding everything being destructed at once: that’s called an arena, and there are crates for it:

https://crates.io/crates/typed-arena

> Regarding everything being destructed at once: that’s called an arena

Thats such a great name :)

It is quite common name for memory pools.

Arenas have more to do with the allocation pattern, they don't solve the cycle problem, right?

You're correct, that crate doesn't solve the cycle problem. There is a different way of doing arenas in Rust that does though.

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.

In a sense, they solve the cycle problem in Rust. The trick is that once something is allocated to an arena, it has the same lifetime as the whole arena, and that allows cyclical links because none of the nodes "outlive each other".

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.

> a weak reference inside a refcell,

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.

Thank you. I will look into these and give it another try.

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.

In Haskell it is easy, you can not create cyclic data structures ;-)

Huh? Sure you can.

Cyclic data structures can be created in Haskell, in large part due to laziness.

If you see data structures as cyclic, it is not "in large part due to laziness", but _only_ due to laziness. If you look at the memory representation I think (but I am not sure) there will be no cycles between allocated objects. Only a thunk.

Using 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.

Counterexample:

    $ 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]

You can take as many as you like. (The 'ones' list contains a tail which links back to its head, producing an infinite list.)

Obviously, this is a trivial example, you can do much more interesting things with mutually recursive bindings.

    let cycle = "cycle " ++ cycle

Frankly, I'd just use unsafe pointers for the backrefs, and wrap the tree API up in a typesafe layer, and build on top of that.

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.

I'd take a similar approach. After all `unsafe` use cases include the implementation of data structures.

I've argued this issue before.

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.

A hashmap being implemented on top of vectors is a pretty common implementation. Not sure what Rust uses though.

Problem is avoiding having to do Vec<Option<T>>

If T is a reference type, doesn't Rust do an optimization where <Option<T>>> is implemented by using null pointers?

Yes. This optimization is expected to be expanded in the future but there are currently "NonZero" types. Rust notices this and uses the zero value as the enum descriminant.

So in this case the code generated is idential to a nullable pointer.

Yes, but that doesn't help when T is not a reference type.

If it's not a reference type, then the Option enum value is probably small relative to the rest of the data in the type.

Option<i32> is 8 bytes

IIRC, Rust's HashMap uses a single raw vector containing for each entry its hash code, its key, and its value; empty entries have a special hash code as a marker, with the key/value left uninitialized. Also, the hashes are kept together (separate from the rest) for better cache behavior during the linear probing.

Wouldn't that be two parallel vectors? (Side note: nobody ever thinks to bring up cache behavior in interviews where I ask about how a hash map could be implemented - it's nice to know that the library writers care :) )

How does that special hash marker work? What happens when something actually hashes to it? Just silently increment the hash?

> Wouldn't that be two parallel vectors?

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).

Oh, clever. Of course you can do it that way.

Good Map implemented on top of Vec: https://github.com/bluss/ordermap

Very nice.

This is a PHP map, correct? It is the one language feature that made PHP stand out from the crowd.

Python has followed suit

> The answer isn't generics, Coq, or some fancy type system nobody will understand or use properly.

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.

Is that a fancy <x> system that nobody will understand or use properly? (Honest question)

We intend for it not to be; more on that as we get closer to actually having a model.

Probably. I used to do formal proof of correctness work and headed a project to build a verifier.[1] That stuff is very hard.

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.

[1] https://github.com/John-Nagle/pasv

> 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.

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.

We built verification into the language in Pascal-F, 30 years ago.[1] That's rarely been done since in real-world imperative languages. It's much easier to keep the verification statements correct if they're in the same file and the same language as the program.

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

> We built verification into the language in Pascal-F, 30 years ago.

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.

What book was that?

> Before you can even consider verifying something, you have to be able to talk about it in some formal language.

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).

Proofs and specifications are different things. Users need to be able to read specifications. For example, if you want to talk about definedness for arrays, a predicate

    defined(arrayname, lowbound, highbound)

is helpful. That goes in assert statements. It's run-time checkable, if you have some extra state in the form of "is defined" flags. But you'd rather prove it once so the run-time checks are unnecessary. With a few simple theorems, such as

    defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1)

and a simple automated prover, you can deal with most of the issues around partially defined arrays.

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.

> That goes in assert statements. It's run-time checkable

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)

is a theorem. It looks like this in Boyer-Moore theory:

    (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

inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme:

      (AND (IMPLIES (LESSP J I) (p A I J))
           (IMPLIES (AND (NOT (LESSP J I))
                         (p A (ADD1 I) J))
                    (p A I J))).

Linear arithmetic informs us that the measure (DIFFERENCE (ADD1 J) I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new formulas:

    Case 3. (IMPLIES (AND (LESSP J I)
                          (ARRAYTRUE A I J)
                          (EQUAL (ALLTRUE (SELECTA A (ADD1 J)))
                                 T))
                     (ARRAYTRUE A I (ADD1 J))),

which simplifies, rewriting with ARRAYTRUE-VOID-RULE and SUB1-ADD1, and opening up ARRAYTRUE and LESSP, to the following eight new conjectures:

...

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

And yes, there's a machine proof that this terminates.

> defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. (proof)

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.

> > 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.

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).

> That's the same thing. It's just a matter of it being automated.

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.

This is being worked on! Several bits of the rust standard library have already been proven safe in the initial model.

In the meantime, Rust's support for automated tests is great.

Alas, tests aren't proofs.

Yet, tests are still useful!

Not if the goal is to prove that an algorithm meets a specification, which is more often than not my goal.

This is why, as a user of GC languages, I think a bit sad that the ergonomics are so bad for cyclic data structures, that this solution is most likely what the majority will turn to.

Thr majority never need to write a cyclic data structure, because they can use an existing one from a library.

Assuming it covers their use case, regarding API definition and O(n) expectations.

Quite often in Rust, the way to make it easier is to go one step back: instead of thinking about how to make a tree right, you might want to think about why you want a tree in the first place. Sometimes it's the right thing to do, sometimes there is another approach that fits Rust's paradigm better.

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.

> instead of thinking about how to make a tree right, you might want to think about why you want a tree in the first place.

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.

Have you considered leveraging crates.io? I'm not sure of your exact constraints, but I've heard some good things about petgraph: https://crates.io/crates/petgraph . It sounds like you might also want to check out some implementations of arenas.

It's fairly easy to do this kind of thing using an arena and indices instead of pointers. Here's a simple splay tree with uplinks implemented this way:

https://github.com/stjepang/vec-arena/blob/master/examples/s...

I think I would just put all the nodes into a Vec and use indices instead of references. This results in every node having the same lifetime, like you wanted. It is what the specialized graph libraries like petgraph are doing, and it is memory safe due to bound checks.

Reply on news.ycombinator.com