D enters Tiobe top 20

[Ola Fosheim Grøstad]

On Sunday, 10 November 2019 at 02:51:53 UTC, Doc Andrew wrote:
> I think you'd just have to wait until all the CTFE and template 
> stuff is done before you start generating VCs. It might not be 
> a deal-breaker, but that's speaking from ignorance, frankly.

Also keep in mind that you have to deal with exceptions, so you 
have to introduce a lot of branching code (unless the verifier 
does that rewriting for you).

> Oh I dunno, aside from adding some extra contracts and avoiding 
> certain language constructs* (like goto), not much really has

You can allow gotos (at least the most common usage). Deal with 
it the same way you model exceptions.

> * Granted, those "certain language constructs" may end up being 
> an insurmountable barrier, where the formally verifiable subset 
> of D is stripped of so many features that it isn't really worth 
> it. Too early to tell.

Well, I think that modular ints is an issue that may make some 
cases harder, but I think most constructs can be modelled in a VC 
language. Still a lot of work.