forall statement and expression syntax gratuitously inconsistent -> horrible error messages LOW SEVERITY

[kjx]

Dafny version

4.6.0

Code to produce this issue

forall x <- xs :: x > 10 by {
   reveal someRandomThing();
}

///yes I have lots of these things. 
///yes they take up quite a lot of time, and more irritation

Command to run and resulting output

bluebook:~ kjx$ "/usr/local/share/dotnet/dotnet" "/Users/kjx/.vscode/extensions/dafny-lang.ide-vscode-3.3.0/out/resources/nightly-2024-05-05-55d1c40/github/dafny/Dafny.dll" "run" "--no-verify" "/Users/kjx/work/dafny/wont-2.dfy"
work/dafny/wont-2.dfy(5,0): Error: this symbol not expected in Dafny
  |
5 | forall x <- xs :: x > 10 by {
  | ^

What happened?

at the very least: "this symbol not expected at this point in your program" :-) not "not expected [at all, ever] in Dafny"

also: why does forall statement use "old-ish" syntax forall x | x in xs not newer forall x <- xs why ensures not :: why no by between the expression and the justification block
(compare assert e by {}, especially assert forall x <- xs :: e by { justification(); } versus pretty much the same thing forall x <- xs ensures e { justification(); }

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

Thanks for the feedback. I believe you're correct that the current behavior is confusing. I believe intuitive syntax is critical for a compelling language and I hope we can prioritize improving this. If you have suggestions for what it should look like, they're very welcome.

[keyboardDrummer]

Marking as enhancement instead of bug, since this is documented behavior.

[robin-aws]

also: why does forall statement use "old-ish" syntax forall x | x in xs not newer forall x <- xs

FWIW you can definitely use the new syntax in forall statements too, it's just the other syntax mismatches that made it look unsupported:

forall x <- xs ensures x > 10 {
   reveal someRandomThing();
}

[kjx]

hah. good to know that at least...