D enters Tiobe top 20
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Sun Nov 10 13:39:23 UTC 2019
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.
More information about the Digitalmars-d