Yeah dropck is a fun little gem, which has received several post-1.0 revisions due to soundness problems.
I agree the system you propose would be simpler in terms of spec and effort, but I don't know about simpler to use. Much like removing mutable references in favour of `foo(X) -> X` would be a simpler type system, but awful to use compared to `foo(&mut X)`.
The simplest system to use is unrestricted references with some form of automatic garbage collection. If you decide that you want a type system that statically tracks resource utilization, why stop halfway at something that only partially solves the problem? I guess you could one-up linear types here and ask for a type system that makes all creation and destruction of information explicit, e.g. https://www.cs.indiana.edu/~sabry/papers/reversible-logic.pd..., but this is probably a more useful route to explore for a hardware design language than a software programming language.
> If you decide that you want a type system that statically tracks resource utilization, why stop halfway at something that only partially solves the problem?
Because there's a tradeoff between ergonomics and static guarantees. A hybrid system (in this case, static tracking of ownership combined with automatic resource destruction) is a valid choice to balance the upsides and downsides of each extreme.
I'm not particularly educated in this issue, but if you're going to use a garbage collector, why not just use a language with a GC that abstracts away memory management completely? Like, what would be the advantages over Java?
I agree the system you propose would be simpler in terms of spec and effort, but I don't know about simpler to use. Much like removing mutable references in favour of `foo(X) -> X` would be a simpler type system, but awful to use compared to `foo(&mut X)`.