This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.
Dafny’s expressiveness tends to be more in the service of coherent specifications and less in the service of language abstraction for its own sake.