Use where instead of var for expressions

[keyboardDrummer]

I don't like var expressions, because var is already used in statements so it can make code that is an expression look like a statement:

var x := ..
var y := ..
// are we inside an expression or a statement? it's impossible to tell from there
x := 3 // error: a let-bound variable can not be re-assigned. Aha, we were in an expression!

Also, while for statements the order of code affects the semantics, for expressions it does not, so it is no longer necessary for the definition of variables to come before their usage. I think it is more readable for the definition to come after the usage, since the name is used as a summary of the body, allowing one to read the code top-down.

I propose the following syntax:

function Foo(x: int): int =>
  x + y 
where 
  x := y + z;
  y := 2;
  z := 3;

Where bindings are checked for cyclic dependencies.

Note that I've also replaced the curly braces around the function body with a =>, which Dafny also uses as part of defining lambda expressions. I think this change makes it extra clear that the body of a function is not a statement. I think beginning Dafny users are often confused because they can not use statements inside function bodies, since the curly braces imply that they can.

[robin-aws]

I love the motivation here at least. Avoiding braces in expressions would also help avoid the ambiguity of {...} between blocks and set displays.

The main thing I don't love in the proposed syntax is the fact that the where "statements" (and we'd have to still allow lemma calls etc) are evaluated top-down, but then the final expressions is up top before all of them. I might prefer something like:

function Foo(x: int): int =>
  let 
    x := y + z;
    y := 2;
    z := 3;
  in
    x + y

That style is super common in functional languages, and it's a smaller syntactic change just localized to mostly StmtExprs, which also improves readability and compactness in compound expressions in statement contexts, like (let x := x := y + z; y := 2; z := 3; in x + y)

[keyboardDrummer]

The main thing I don't love in the proposed syntax is the fact that the where "statements" (and we'd have to still allow lemma calls etc) are evaluated top-down, but then the final expressions is up top before all of them.

Good point, I think this only makes sense if you don't need expression statements at all. Suppose you wouldn't need them, would the top-down order then make sense to you?