Module Definitions
Modules are stateless containers for organizing related functions, types, constants, and proof helpers into reusable units. They are the right place for reusable pure functions and typed interfaces that actors can call.
Import Syntax
Imports bring modules, types, and functions from other files into scope. In verified code, imports are also a modular proof boundary: callers prove imported preconditions and rely on imported postconditions instead of reopening the imported body.
Module Types
Module types describe the required structure of a module using structural typing. They are useful for parameterized proof code, dependency injection, and first-class module APIs, but they are still subject to Sector9's runtime/proof boundary checks.
First-Class Modules
Modules are first-class values in Sector9: you can pass them as function parameters, return them from functions, store them in variables, and select between them conditionally. Verification follows the module type and member contracts through those indirections without turning the module into an actor boundary.