D enters Tiobe top 20

[Timon Gehr]

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