PS: собственно dafny - это "WhyML" с человеческим лицом

[kouzdra]

Одна из причин моего к нему интереса - именно что "вроде бы на этом можно писать" (потому что на WhyML писать невозможно - да собственно и не предполагалось - его делали для опытов с доказательством всяких достаточно навороченных алгоритмов).

Так-то там ничего особенно принципиально нового нет.