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.
Comments and Documentation
Sector9 supports single-line comments, multi-line block comments, and documentation comments. Ordinary comments help readers but do not participate in type checking, verification, or runtime output. Documentation comments are also source metadata: they can feed generated docs and directives such as @deprecated.
Printing and Debugging
Sector9 provides Debug.print for development-time output and debug_show for converting values to text. In verification, debug output itself is erased, but argument expressions are still checked and evaluated for their normal proof obligations.