Premise

Premise allows you to enforce static constraints on values, catching potential bugs before your code even runs.

Compile-time Validation

In its basic usage, a premise is verified during compilation. By shifting validation from runtime to compile-time, AERIS ensures safety without performance overhead.

fn receive_password(password: String) {
  let len = password.len();
  premise len >= 12 and len <= 128;
  println(password);
}

fn main {
  receive_password("HelloAERIS123"); // Ok
  receive_password("pswd1234"); // Compile Error: Length (8) is less than 12
}

Note: If a value can be proven to violate the condition, AERIS will trigger a compile-time error, preventing the build from succeeding.

Runtime Integration

For values that can only be known at runtime (such as user input), use the sat keyword. It allows you to safely bridge dynamic data with your static premises.

import stdin from std/io

fn receive_password(password: String) {
  let len = password.len();
  premise len >= 12 and len <= 128;
  println(password);
}

fn main {
  let input = stdin.read_line();
  receive_password(sat input)
  else {
    println("Invalid password!");
  };
}