Introduction
1.
Build System
1.1.
Project Structure
1.2.
Manifest File Format
1.3.
Module System
1.4.
Dependency Resolution Strategy
2.
Syntax and Semantics
2.1.
Comments
2.1.1.
Line
2.1.2.
Block
2.2.
Identifiers
2.3.
Paths
2.4.
Flow Control Structures
2.4.1.
Block
2.5.
Types
2.5.1.
Primitive
2.5.1.1.
nothing
2.5.1.2.
bool
2.5.1.3.
u8
2.5.1.4.
u16
2.5.1.5.
u32
2.5.1.6.
u64
2.5.1.7.
usize
2.5.1.8.
i8
2.5.1.9.
i16
2.5.1.10.
i32
2.5.1.11.
i64
2.5.1.12.
isize
2.6.
Expressions
2.6.1.
Literal
2.6.1.1.
Boolean
2.6.1.2.
Integer
2.6.2.
Item
2.6.3.
Call
2.6.4.
Syscall
2.6.5.
Block
2.7.
Specifications
2.7.1.
Propositions
2.7.2.
Assumes
2.7.3.
Requires
2.7.4.
Ensures
2.8.
Statements
2.8.1.
Import
2.8.2.
Export
2.8.3.
Function Definition
2.8.4.
Expression
2.8.5.
Block
2.9.
Complete Grammar
2.10.
Name Resolution
2.11.
Type Checking
2.12.
Type Inference
Light (default)
Rust
Coal
Navy
Ayu
The Protocol Verification Language Reference
Types
Syntax
<type> ::= <primitive-type>
Semantics
Typing is
strong
and
static
.