Confusing message for out parameters for new users

[MikaelMayer]

We got several confused new Dafny users that, in the following program:

method Callee() returns (i: int) {
  i := 0;
}
method Caller() {
  Callee();
}

would not understand the error message

wrong number of method result arguments (got 0, expected 1)

because they are passing the correct number of arguments to the method.

What is confusing is actually

• They skip the word "result"
• In no other language I know is there such a thing of returning multiple values (not out parameters), so this is very novel.
• We are calling these parameters which should be to the left of the method "result arguments", which is weird. Arguments are passed usually to the right of the method name inside parentheses. At best, result arguments should be prefixed with "out" like in C#. However, here they are not arguments.

Here are alternative messages that could help reduce the friction for new users

• 1️⃣ The method returns 1 value(s) but is assigned to 0 variable(s). All return values must be assigned.
• 2️⃣ Wrong number of assignment variables to store the result of the method (expected 1, got 0)
• 3️⃣ The number of assignment variables is not the same as the number of return values (expected 1, got 0)
• 4️⃣ Mismatch between returned values (1) and assignments (0)

Please add your alternatives and/or vote so that we can make a better error message

Update
Based on three votes, we choose

The method returns 1 value(s) but is assigned to 0 variable(s). All return values must be assigned.

[keyboardDrummer]

The term "result parameter" is difficult to interpret for me. I would prefer "return value".

Option 1 seems great. Consider adding a sentence "All return values must be assigned"

[MikaelMayer]

Good catch for "result parameter" instead of now "return values" in option 3. See, even I am biased towards the Dafny language, it's good that we have these discussions just to realized how awkward a dialect might seem.

I also added "All return values must be assigned" to option 1, which I think adds value.

[davidcok]

I vote for #1