dafny-lang/rfcs

Dafny request-for-feature discussions

rfcs

Dafny request-for-feature discussions

rfcs's Issues

RFC pending: Unicode string support

To address the issues enumerated in dafny-lang/dafny#413

RFC pending: deeper testing support in Dafny

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. :)

Github Discussions

I came here looking to leave some feedback after trying out Dafny, but the Gitter chat is dead and you apparently shut down the mailing list. Github has a new self-contained discussions feature, why don't you give that a shot? Without the ability to at least bounce pre-RFC ideas around, you are unlikely to get much engagement here.