Prototype of Ownership/Borrowing System for D

[Doc Andrew]

On Friday, 22 November 2019 at 06:43:01 UTC, mipri wrote:
>
> I'd sell it not as "it forces you to test" but "it reliably
> promotes nullable types to non-nullable types when this is safe"
>
> Kotlin example:
>
>   fun Int.test() = println("definitely not null")
>   fun Int?.test() = println("could be null")
>
>   fun main() {
>       val n: Int? = 10
>       n.test()
>       if (n != null)
>           n.test()
>   }
>
> Output:
>
>   could be null
>   definitely not null
>

That's pretty cool.

> So if you test a nullable type for null, everything else in the
> control path works with a non-nullable type. The effect on the
> program is that instead of having defensive tests throughout 
> your
> program, you can have islands of code that definitely don't 
> have to
> test, and only have the tests exactly where you need them. If 
> you
> go too far in not having tests, the compiler will catch this as 
> an
> error.
>
> I've never used TypeScript, but Kotlin's handling of nullable 
> types
> is nice to the point I'd rather use the billion dollar mistake 
> than
> an optional type.

Yes, after all, pointers are already an "optional" type, where 
null stands in
for None (or whatever).

>
> IMO what's really exciting about this though is that the 
> compiler
> smarts that you need for it are *just short* of what you'd need 
> for
> refinement types, so instead of just
>
>   T?  <-- it could be T or null
>
> you can have
>
>   T(5) <-- this type is statically known to be associated with 
> the
>            number 5.
>
> And functions can be defined so that it's a compile-time error 
> to
> pass a value to them without, somewhere in the statically known
> control path, doing something that associates them with 5.
>
> Similarly to how you can't just hand a char[4] to a D function 
> with
> a signature that's asking for a char[5] - but for any type, for 
> any
> purpose, and with automatic promotion of a char[???] to char[5] 
> in
> the same manner that Kotlin promotes Int? to Int
>
> Add a SAT solver, and "this array is associated with a number 
> that
> is definitely less than whatever this size_t is associated 
> with",
> and you get compile-time guarantees that you don't need bounds
> checking for definite control paths in your program. That's 
> cool.
> ATS does that: it's a compile-time error in ATS to look at 
> argv[2]
> without checking argc.

Standby for some more discussion on formal verification... :)

I'm working on a program I'm calling ProveD (for now, at least) 
to do source-to-source translation using libdparse to generate 
Why3ML code and verification conditions that can be proven with 
Why3 and whatever SMT solvers you have installed. I don't have 
much to show yet, but I should have a PoC that others can hack on 
in a few months.

A lot of the effort I've spent on it so far is fighting with 
Ubuntu's broken Why3/Z3/Alt-Ergo/CVC4 packages (pro tip: don't 
use them) and goofing around with the OCaml package manager OPAM 
to get everything set up to where I can start running proofs.

I was going to try and get a little further before starting a 
thread for discussion, but if it comes up as a result of "The 
null Thread", that might be a good place to start.

-Doc