Prototype of Ownership/Borrowing System for D

[aliak]

On Sunday, 1 December 2019 at 14:44:25 UTC, Timon Gehr wrote:
>> Rust has done a pretty good job selling safety as a compile 
>> time phenomenon.
>
> I have no interest at all in how Rust is marketed. Rust has 
> bounds checks and runtime checks against unsafe borrowing, 
> because its type system is not expressive enough to formalize 
> functional correctness properties.

Can you elaborate on this a bit more? Which correctness 
properties of functions cannot be formalized by rust's type 
system and what particularly is lacking in it's type system to be 
able to do that?

If you have any links handy that can explain these concepts also 
that'd be super appreciated.

Also, can D's type system become expressive enough without being 
too crazy to solve the same?