Prototype of Ownership/Borrowing System for D

[Timon Gehr]

On 01.12.19 16:35, aliak wrote:
> 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

Most of them. E.g., Rust's type system cannot prove that an index is 
within bounds of a std::vec::Vec.

> and what particularly is lacking in it's type system to be able to do that?
> ...

E.g., dependent types.

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

https://softwarefoundations.cis.upenn.edu/

> Also, can D's type system become expressive enough without being too 
> crazy to solve the same?
> 
In principle, yes. But I am not aiming for this at the moment. Also, 
people have different ideas about what "too crazy" means.