RFC pending: deeper testing support in Dafny

[robin-aws]

For visibility and tracking, I'm planning on writing an RFC that goes deeper than the current support for the expect keyword and the {:test} attribute I added a while back.

@seebees has convinced me that there is a lot of benefit in having Dafny let you support specifications with testing instead of or in addition to verification, for cases where verification is difficult (especially for new Dafny users) or impossible (e.g. external code). I expect the RFC will have to examine several alternatives for how to achieve this, but we're convinced that this is a worthwhile goal and that at least one potential solution exists.

I've been throwing around the term "gradual verification" for this. :)