dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

Feature request: Const declarations in methods and functions #5946

Open MikaelMayer opened 2 days ago

MikaelMayer commented 2 days ago

Following the ideas of this video https://youtu.be/f74PSgwLdDk?si=M5llP57gTIwiw3dA&t=969

We wish to have

method Test() {
  const x := 2;
  x := x + 1; // Error !
}

that could prevent accidental rewrite of a variable, like in JavaScript, or Rust (let without mut)

Similarly, in functions, we could benefit from this syntax and deprecate the "var" there, since variables are not overridable by default.

function Test(): int {
  const x := 2
  x
}

The semi-colon could be optional for functions.

MikaelMayer commented 2 days ago

Related to https://github.com/dafny-lang/dafny/issues/5914