D enters Tiobe top 20
paolo.invernizzi at gmail.com
Fri Nov 8 13:09:27 UTC 2019
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.
>> "... 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
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
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!
More information about the Digitalmars-d