November 07, 2019
On 11/7/19 12:41 PM, Timon Gehr wrote:
> On 07.11.19 08:34, drug wrote:
>> On 11/7/19 3:00 AM, Walter Bright wrote:
>>> Not that this is necessarily a bad thing, as I also promote the safe/unsafe code dichotomy.
>>>
>> And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
> 
> http://plv.mpi-sws.org/rustbelt/

Thanks for the link. The project aims to the problem I've mentioned above and can really have a big impact.
November 07, 2019
On Thursday, 7 November 2019 at 00:00:28 UTC, Walter Bright wrote:
> 
>
> D needs to make @safe the default, though.

In terms of a timeline, can I assume that there are no plans for this until a D 3.0?
November 07, 2019
On Thursday, 7 November 2019 at 11:33:35 UTC, jmh530 wrote:
> On Thursday, 7 November 2019 at 00:00:28 UTC, Walter Bright wrote:
>> 
>>
>> D needs to make @safe the default, though.
>
> In terms of a timeline, can I assume that there are no plans for this until a D 3.0?

https://github.com/dlang/DIPs/pull/166
November 07, 2019
On Thursday, 7 November 2019 at 12:06:07 UTC, Mike Parker wrote:
>> [snip]
>> In terms of a timeline, can I assume that there are no plans for this until a D 3.0?
>
> https://github.com/dlang/DIPs/pull/166

Ah, I hadn't realized a DIP was in the works. Given that it is a Walter DIP, that means it has a high likelihood of being accepted...
November 07, 2019
On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
> On 07.11.19 08:34, drug wrote:
>> On 11/7/19 3:00 AM, Walter Bright wrote:
>>> Not that this is necessarily a bad thing, as I also promote the safe/unsafe code dichotomy.
>>>
>> And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
>
> http://plv.mpi-sws.org/rustbelt/

"... Any realistic languages targeting this domain in the future will encounter the same problem ..."

I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.
November 07, 2019
On 11/7/2019 7:34 AM, Paolo Invernizzi wrote:
> On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
>> On 07.11.19 08:34, drug wrote:
>>> On 11/7/19 3:00 AM, Walter Bright wrote:
>>>> Not that this is necessarily a bad thing, as I also promote the safe/unsafe code dichotomy.
>>>>
>>> And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
>>
>> http://plv.mpi-sws.org/rustbelt/
> 
> "... Any realistic languages targeting this domain in the future will encounter the same problem ..."
> 
> I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.

I don't see anything on that site that contradicts what I wrote. In particular:

"Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art."

is saying the same thing.
November 08, 2019
On 08.11.19 04:43, Walter Bright wrote:
> On 11/7/2019 7:34 AM, Paolo Invernizzi wrote:
>> On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
>>> On 07.11.19 08:34, drug wrote:
>>>> On 11/7/19 3:00 AM, Walter Bright wrote:
>>>>> Not that this is necessarily a bad thing, as I also promote the safe/unsafe code dichotomy.
>>>>>
>>>> And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
>>>
>>> http://plv.mpi-sws.org/rustbelt/
>>
>> "... Any realistic languages targeting this domain in the future will encounter the same problem ..."
>>
>> I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.
> 
> I don't see anything on that site that contradicts what I wrote. In particular:
> 
> "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art."
> 
> is saying the same thing.

Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future.

There is also this recent work on functional verification of safe Rust code: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf
November 08, 2019
On 11/7/2019 1:45 AM, Timon Gehr wrote:
> That's not a plus. It will _mean_ something else. Therefore, you will have trouble at the interface between @live and non-@live code, because it is not the same language. Not to mention that @live without any further syntax changes will necessarily be even more restrictive than safe Rust.

I guess we'll have to see. I'm making progress every day on it. I'm looking forward to you tearing it apart :-)
November 08, 2019
On 11/8/2019 2:09 AM, Timon Gehr wrote:
> On 08.11.19 04:43, Walter Bright wrote:
>> I don't see anything on that site that contradicts what I wrote. In particular:
>>
>> "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art."
>>
>> is saying the same thing.
> 
> Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future.

I read it as ensuring the interface to the unsafe code is correct, not the unsafe code itself. I.e. "is properly encapsulated".

After all, if the unsafe code can be proved correct, then it is no longer unsafe, and Rust's ownership/borrowing system can be dispensed with entirely as unnecessary for safety.

I'm happy to let the CS Phd's work on those problems, as I am way out of my depth on it.

I've convinced myself that the Ownership/Borrowing notion is sound, but have no idea how to formally prove it.

> There is also this recent work on functional verification of safe Rust code: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf

I don't see any reason why the techniques used in the paper wouldn't work on D, given O/B.

Note that the paper says: "We do not address unsafe code in this paper".
November 08, 2019
On Friday, 8 November 2019 at 10:25:44 UTC, Walter Bright wrote:
> After all, if the unsafe code can be proved correct, then it is no longer unsafe, and Rust's ownership/borrowing system can be dispensed with entirely as unnecessary for safety.

They probably mean that it is verified with human provided guides.

A human must annotate the library with carefully chosen asserts that the verifier will prove one-by-one until they can all be disposed of. So you have to understand that verification engine and carefully "nudge" it until it succeeds.

So, mostly suitable for the standard library and simple third party libraries, but not for bleeding-edge applications that keep changing...