D enters Tiobe top 20

[Paolo Invernizzi]

On Friday, 8 November 2019 at 03:43:56 UTC, 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.

Agreed, and I definitely appreciate your effort in pushing 
towards mechanic verification on that topic.

What I mean is that there will be the need for manual 
verification also, when libraries will be forced to rely on 
unsafe code.

To my understanding, the project is providing guidance in doing 
that (manual) verification of unsafe code.

My advice is to work tightly coupled with Timon, to have a clear 
understanding of what is theoretically feasible and what not, for 
mechanical check, and to try to have clear borders around the two 
arenas.

In that way, you can concentrate on implementing and polishing 
what is pragmatically doable in the compiler, in a mechanical 
way, avoiding efforts towards dead ends.

But hey, you have already surprised us all when you designed D 
... I will be glad to see that your idea really works!

/Paolo