On Borrow Checking

[Timon Gehr]

On 5/4/25 03:30, Walter Bright wrote:
> On 5/3/2025 2:47 PM, Timon Gehr wrote:
>> It does not.
> 
> See my other reply regarding higher level pointer constructs.
> ...

Well, let's continue that discussion in the other subthread.


> 
>> Whether a safety check is "needed" depends on what invariants the type 
>> system is able to establish and rely on in `@safe` code.
> 
> If you can enumerate the other safety checks D needs to be memory safe, 
> I'm listening.

E.g., null checks. x)

My point is that this is an _inductive invariant_. You have to state 
what the invariant is, then you must prove that all execution steps of 
the program maintain this invariant and in turn you can rely on the 
invariant holding when you show memory safety.

This is a _design problem_. You don't _need_ any compile-time checks to 
have a memory safe language, you just need them if there are 
performance/expressiveness considerations.

`@safe` with DIP1000 and GC is fine in terms of memory safety, ignoring 
some bugs. It's just not very expressive.

`@live` does not add additional expressiveness to memory safe D, there 
is no new `@safe` code that it enables. This is because it does not 
actually expand the type system invariant in a way that could then be 
relied upon.