[mafribe]

   Destructors seem to be a 
   pain point 

The problem is not so much typing as such (things that don't return anything but terminate -- as destructors do -- can be typed as Unit) but rather to find a good trade-off between expressivity of the language and simplicity of the typing system.

Basically explicit destructors mean the typing system needs to track lifetimes and ownership in some form or shape. There seem to be two main options.

- Simple lifetime/ownership scheme, but then you need a garbage collector anyway, and that it's mostly pointless to have explicit destructors. Just let every variable be cleaned up by the GC makes for a simpler language (under the hood clever escape analysis might be used for stack allocation of variables that don't escape their activation context).

- Avoid a GC, but then you need a complex typing system with unique owners to have any chance at expressivity (and you still need unsafe blocks and reference counting). This is Rust's choice.

Another issue is how consistently to combine destructors with other effects, in particular exceptions.

   Pointer/backpointer pairs 
   need to be a language level 
   concept.

As "JoshTriplett" also suggests, this is certainly an interesting idea, but I don't think a compelling choice has been found yet.

[Animats]

Think of backpointers as a combination of Rust optional pointers and weak pointers, mostly checked at compile time. The basic rule for backpointers is this: If an type instance A contains a backpointer P1, it must either be a None, or a reference to a type instance B which has exactly one reference P2 to A.

Checks required:

- P2 cannot be changed when P1 is not None. (Run-time check; the compiler has to recognize when it is necessary.)

- P1 can only be set to None or B. (Compile-time check)

- P1 must be set to None before B is destroyed. This avoids a dangling pointer. (Compile-time check when possible, otherwise run-time check.)

- Borrow checking must treat a borrow using P1 as a borrow of B.

These simple rules would maintain the invariant for the backpointer. This allows doubly-linked lists without unsafe code. The backpointer is "weak" and doesn't count as ownership. It's basically weak pointers with a count of either 0 or 1.

[mafribe]

I'm not saying this can't be done, au contraire! Indeed cost coherent programming idioms can be converted into typed language primitives. But there is a price to pay in terms of typing system complexity.

It's a slippery slope argument: if you add this, why stop there? Especially if you require run-time checks.

If there was a compelling set of operation that preserved the invariants without run-time checks, and it was expressive, i.e. it covered a large number of cases that you'd otherwise had to put into "unsafe" and it didn't ruin type inference ...