Available in native alpha.13
panack explain shows the facts behind a natural-number subtraction check and the decisions behind local call and await effect boundaries. Read the compiler’s evidence alongside its ordinary diagnostics.
Save this program as remaining.panack, then run the command below with the native alpha.13 toolchain. The command checks the whole project and reports evidence for the named function. It does not execute your program or emit bytecode.
The true branch establishes that n is at least 2. The compiler uses that lower bound to prove the subtraction cannot go below zero.
pure remaining(n: Nat): Nat {
if n >= 2 {
n - 2
} else {
0
}
}
main(): Void {
print(remaining(5))
}
Output
3
panack explain remaining.panack --function remainingThe 3 above is the program’s output when run. The explanation command instead reports this excerpt:
program: accepted function: remaining scope: Nat subtraction; generic definitions, not call-site specialisations subtraction: proved source: project/remaining.panack:3:5-3:10 expression: n - 2 operand types: Nat, Nat obligation: left >= right right constant: 2 left lower bound: 2 guard branch: true source: project/remaining.panack:2:6-2:12 expression: n >= 2 reason: retained lower bound is at least the right constant
Read program: accepted as whole-project acceptance. subtraction: proved describes this one obligation. The source positions connect the decision to the subtraction and its guard.
Change n - 2 to n - 3, keeping the guard n >= 2. Run the same explanation command again. The lower bound is no longer sufficient, so the program is rejected and the subtraction is unproved. That means the checker could not establish safety; it is not a claim that the program was executed and failed.
Save this deliberately invalid program as report.panack. A pure function cannot call the effectful print builtin.
pure report(): Void {
print(1)
}
main(): Void {}
panack explain report.panack --function reportThe command exits with status 1, preserves the ordinary diagnostic on stderr, and includes this local explanation:
program: rejected effect scope: local call and await boundaries; declarations and callable types, not transitive/runtime effects effect boundary: rejected source: project/report.panack:2:3-2:11 expression: print(1) boundary: call context: pure callee: print classification basis: builtin or constructor contract callee effect: ordinary awaited: no reason: pure function cannot call impure function print
An ordinary function may print. Changing pure report to report makes this call boundary allowed. Allowed describes that local boundary; consult the separate program result for whole-project validity.
Subtraction evidence comes from the checker’s existing constants and lower-bound facts. The query adds visibility to those decisions; it does not add proof rules.
Effect evidence describes local calls and await boundaries, including pure, ordinary and async contexts. It does not follow callee bodies to infer transitive or runtime effects.
Unsupported cases and missing evidence are explicit. A function with no relevant subtraction or call may be accepted and still have nothing supported to explain.
Accepted projects exit 0. Rejected projects and invalid queries exit 1. A local proof does not override other errors. Alpha.13 also records supported decisions for values, calls, returns, assignments, operators, conditions, matches, collections and record fields. This guide illustrates subtraction and effects. Complete checker coverage, source-to-bytecode explanations and runtime value histories remain outside the released contract.
This guide applies to native alpha.13. The pinned browser playground does not provide this CLI command. Read the full query contract → · See what alpha.13 delivers →
Keep exploring