D enters Tiobe top 20

[Ola Fosheim Grøstad]

On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
> With the way we do multi-threading now, where anything goes, 
> absolutely. SPARK can formally verify multi-threaded tasks but 
> using a fairly restrictive model (Ravenscar). I don't think 
> performance goes absolutely in the tank with Ravenscar, but 
> yeah, if you don't worry about synchronization, ignore race 
> conditions, and just hope for the best, then sure, you're going 
> to win in the benchmarks :)

Ok, so Ravenscar requires tasks to be dispatched in a FIFO 
manner, but you should be able to do better than that if you only 
get to use high level synchronization.

For instance there are people who do verification of distributed 
communication protocols, so if you use some kind of 
message-passing scheme (or equivalent) then those approaches 
would apply.


> It may be that a slightly-different threading model, perhaps 
> like that thread "nursery" idea which has been posted here 
> before

«Structured concurrency» reminds me of rendezvous, i.e. that 
threads wait for each other at certain points, but less flexible.

I'm not really convinced that a "nursery" is easier to deal with 
than futures/promises, in the general case, though.


> One thing that I've looked around for (without much luck) is 
> just using GPUs to speed up the solvers themselves. Apparently 
> parallelizing SAT solvers isn't the easiest thing in the world, 
> but it would be a neat research topic.

There are papers on it, but solvers are sensitive to the 
strategies (heuristics) used... so might be difficult to get 
right on a GPU. You'd probably have to use some kind of hybrid.

I also see that there are papers on FPGA SAT solvers.

> The cool thing is that, with the right proofs in place, you can 
> actually get _faster_ code when formally verified, because all 
> of the normal sanity-checks you do in code can get shifted to 
> compile-time.

Sure, like indexing of arrays (array bounds checks).

> Your point is well taken, but I do hope that we can get proven 
> correctness of bare-metal code without having to write 
> something like Liquid Haskell ;)

Liquid Haskell looks interesting, though.  You might find this 
interesting:

http://leino.science/dafny-power-user/

It gives some hints of where such languages might go.