Variables and Bindings
Sector9 provides two ways to bind values to names: immutable let bindings and mutable var declarations. Choosing the right one affects both code clarity and verification.
Immutable Bindings with let
The let keyword creates an immutable binding. Once assigned, the value cannot be changed:
let x : Nat = 42;
let name = "Alice"; // Type inferred as Text
let pair = (1, 2); // Type inferred as (Nat, Nat)
Attempting to reassign a let binding produces a type error:
let x = 10;
x := 20; // ERROR: expected mutable assignment target
Pattern Bindings
let supports destructuring patterns for tuples:
let (a, b) = (10, 20); // a = 10, b = 20
let (first, _, third) = (1, 2, 3); // Ignore middle with _
Pattern bindings must be irrefutable. Tuple and immutable-record destructuring are supported when the pattern cannot fail. Refutable patterns such as literals and options are rejected:
let (0, y) = pair; // ERROR: refutable pattern not allowed
let (?x, y) = pair; // ERROR: option pattern can fail
let { x } = record; // OK when record has field x
Mutable Variables with var
The var keyword creates a mutable binding that can be reassigned using :=:
var counter : Nat = 0;
counter := counter + 1; // Now counter = 1
counter += 1; // Shorthand: counter = 2
Mutable variables require simple identifiers. Unlike let, patterns are not allowed:
var (a, b) = (1, 2); // ERROR: patterns not allowed with var
Local vs Actor-Level Variables
Variables can be declared at two scopes:
Local Variables
Declared inside function bodies, local variables exist only for that function call:
public func compute(n : Nat) : async Nat {
let doubled = n * 2; // Immutable local
var sum = 0; // Mutable local
sum := sum + doubled;
sum
}
Actor Fields
Declared at actor level, these persist across function calls:
persistent actor {
var balance : Nat = 0; // Mutable actor field
let rate : Nat = 5; // Immutable actor field
public func deposit(amount : Nat) : async ()
modifies balance
{
balance += amount;
}
}
Actor fields marked with var require modifies clauses in functions that change them.
Mutable Records and Arrays
Mutability also applies to record fields and arrays:
Mutable Record Fields
Records can have mutable fields using var:
type Point = { var x : Int; var y : Int };
let p : Point = { var x = 0; var y = 0 };
p.x := 10; // OK: field is mutable
p.y := 20;
The binding p is immutable (cannot be reassigned), but its fields are mutable.
Mutable Arrays
Arrays can be mutable or immutable:
let immutableArr = [1, 2, 3]; // Immutable array
let mutableArr = [var 1, 2, 3]; // Mutable array
mutableArr[0] := 99; // OK
immutableArr[0] := 99; // ERROR: immutable array
Assignment Operators
Mutable variables support compound assignment:
| Operator | Meaning |
|---|---|
:= | Simple assignment |
+= | Add and assign |
-= | Subtract and assign |
*= | Multiply and assign |
/= | Divide and assign |
%= | Modulo and assign |
var n : Nat = 10;
n += 5; // n = 15
n -= 3; // n = 12
n *= 2; // n = 24
When to Use Each
Prefer let When
- The value should not change after initialization
- You want the verifier to track that a value is constant
- You are destructuring tuples or capturing intermediate results
Use var When
- The value must change during execution (counters, accumulators)
- You need actor-level persistent state
- The algorithm requires updating values in loops
Verification Implications
Immutable Bindings are Simpler to Verify
The verifier can substitute let bindings directly:
let x = a + b;
assert x == a + b; // Trivially true
Mutable Variables Require State Tracking
Changes to var bindings must be reasoned about explicitly:
var x = 0;
x := x + 1;
assert x == 1; // Verifier tracks the update
x := x + 1;
assert x == 2; // Verifier tracks again
Actor Fields Need Footprints
Functions that modify actor-level var fields must declare them in modifies:
persistent actor {
var counter : Nat = 0;
public func increment() : async Nat
modifies counter
ensures counter == old(counter) + 1
{
counter += 1;
counter
}
}
Loop Invariants
Mutable variables modified in loops often require explicit loop invariants:
var sum = 0;
var i = 0;
while (i < n) {
loop:invariant i >= 0 and i <= n;
loop:invariant sum == i * (i + 1) / 2;
i += 1;
sum += i;
}
Ghost Variables
For verification-only state, use ghost var:
persistent actor {
var balance : Nat = 0;
ghost var operations : Nat = 0; // Verification only
invariant operations >= 0;
public func deposit(amount : Nat) : async ()
modifies balance, operations
{
balance += amount;
ghost { operations += 1; };
}
}
Ghost variables are erased from runtime code but available for proofs. See Ghost Variables for details.
Type Annotations
Type annotations are optional when the type can be inferred:
let x = 42; // Inferred as Nat
let y : Int = 42; // Explicitly Int
var z = 0; // Inferred as Nat
var w : Int64 = 0; // Explicitly Int64
For actor fields, explicit types are recommended for clarity:
persistent actor {
var counter : Nat = 0; // Clear intent
var flag : Bool = false; // Explicit type
}
Common Mistakes
Forgetting var for Mutable Fields
// WRONG - field is immutable
type Cell = { value : Int };
let c : Cell = { value = 0 };
c.value := 10; // ERROR
// CORRECT
type Cell = { var value : Int };
let c : Cell = { var value = 0 };
c.value := 10; // OK
Missing modifies Clause
persistent actor {
var x : Nat = 0;
// WRONG - missing modifies
public func update() : async () {
x := 1; // ERROR: no write permission
}
// CORRECT
public func update() : async ()
modifies x
{
x := 1;
}
}
Using Complex Patterns with var
// WRONG - var doesn't support patterns
var (a, b) = (1, 2);
// CORRECT - use separate declarations
var a = 1;
var b = 2;
Summary
letcreates immutable bindings that cannot be reassignedvarcreates mutable bindings that can be updated with:=letsupports irrefutable tuple and record patterns;varrequires simple identifiers- Actor-level
varfields requiremodifiesclauses in functions that write them - Record fields and arrays can independently be mutable with
var - Prefer
letfor simpler verification; usevarwhen mutation is needed - Use
ghost varfor verification-only state