Section 20: Formal Language Grammar and Syntax Definition¶
TECHSPEC-20 — Section 20 · Version 0.1 · Status: Initial Draft
Status: draft. This section is an Initial Draft (Section 57 is a Working Register). It describes intended or proposed behavior, not a finalized, implemented language rule. Do not treat examples here as normative.
1. Grammar Philosophy¶
The language must have a formally defined grammar.
Every valid source construct must follow explicit syntax rules. The compiler must not rely on guessing what the programmer or AI agent intended.
The grammar must be: - Unambiguous. - Consistent. - Machine-readable. - Human-readable. - Versioned alongside the language specification.
2. Grammar Notation¶
The language specification will use Extended Backus-Naur Form (EBNF) to define its grammar.
The following notation is used:
=means a definition.|means an alternative.[ ]means optional.{ }means zero or more repetitions.( )groups expressions." "represents literal source text.;terminates a grammar definition.
3. Source File Grammar¶
The initial source file structure is:
source_file =
module_declaration,
{ import_declaration },
{ declaration },
EOF ;
module_declaration =
"MODULE", identifier ;
import_declaration =
"IMPORT", qualified_name ;
declaration =
type_declaration
| function_declaration
| constant_declaration ;
Every source file must begin with exactly one module declaration.
Imports must appear before declarations.
4. Type Declaration Grammar¶
type_declaration =
visibility,
"TYPE",
identifier,
":",
type_definition ;
type_definition =
struct_definition
| enum_definition
| constrained_type_definition ;
struct_definition =
{ field_declaration },
{ invariant_declaration } ;
field_declaration =
identifier, ":", type_reference ;
enum_definition =
identifier, { identifier } ;
constrained_type_definition =
type_reference,
"WHERE",
expression ;
invariant_declaration =
"INVARIANT",
expression ;
5. Function Declaration Grammar¶
function_declaration =
visibility,
"FUNCTION",
identifier,
"(",
[ parameter_list ],
")",
"->",
type_reference,
{ contract_declaration },
"IMPLEMENTATION:",
statement_block,
"END FUNCTION" ;
parameter_list =
parameter,
{ ",", parameter } ;
parameter =
identifier,
":",
type_reference ;
contract_declaration =
requires_declaration
| ensures_declaration
| effects_declaration
| failures_declaration ;
requires_declaration =
"REQUIRES:",
expression ;
ensures_declaration =
"ENSURES:",
expression ;
effects_declaration =
"EFFECTS:",
effect_list ;
failures_declaration =
"FAILURES:",
type_reference ;
6. Statement Grammar¶
statement_block =
{ statement } ;
statement =
variable_declaration
| assignment
| conditional_statement
| loop_statement
| match_statement
| return_statement
| expression_statement ;
variable_declaration =
( "LET" | "VAR" | "CONST" ),
identifier,
":",
type_reference,
"=",
expression ;
assignment =
identifier,
"=",
expression ;
return_statement =
"RETURN",
expression ;
conditional_statement =
"IF",
expression,
":",
statement_block,
{ "ELSE IF", expression, ":", statement_block },
[ "ELSE:", statement_block ],
"END IF" ;
Additional statement forms will be defined as their semantics are finalized.
7. Expression Grammar¶
expression =
logical_expression ;
logical_expression =
comparison_expression,
{ logical_operator, comparison_expression } ;
comparison_expression =
additive_expression,
[ comparison_operator, additive_expression ] ;
additive_expression =
multiplicative_expression,
{ additive_operator, multiplicative_expression } ;
multiplicative_expression =
unary_expression,
{ multiplicative_operator, unary_expression } ;
unary_expression =
[ unary_operator ],
primary_expression ;
primary_expression =
literal
| identifier
| function_call
| "(",
expression,
")" ;
function_call =
qualified_name,
"(",
[ argument_list ],
")" ;
argument_list =
expression,
{ ",", expression } ;
Operator precedence must be defined explicitly. Parentheses may be used to override normal precedence.
8. Lexical Rules¶
The lexer must recognize:
- Identifiers.
- Keywords.
- Integer literals.
- Decimal literals.
- String literals.
- Character literals.
- Operators.
- Punctuation.
- Comments.
- Whitespace.
Rules:
- Identifiers must follow the language's naming conventions.
- Keywords are reserved.
- The language is case-sensitive.
- Whitespace separates tokens but does not determine program meaning.
- Comments begin with // and continue to the end of the line.
- Invalid characters must produce lexical diagnostics.
- String and character escaping rules must be formally specified.
9. Grammar and Semantic Validation¶
A program that matches the grammar is not automatically valid.
The compiler must separately validate: - Type correctness. - Declaration rules. - Scope and visibility. - Function contracts. - Return paths. - Variable initialization. - Mutability. - Effect declarations. - Permission requirements. - Other applicable language constraints.
Parsing establishes syntactic validity only.
10. Grammar Versioning¶
Grammar changes must be versioned.
Rules: - Every grammar version must correspond to a language version. - Breaking syntax changes require explicit compatibility handling. - The parser must not silently reinterpret unsupported syntax. - Deprecated syntax must produce clear diagnostics. - Grammar examples must be validated against the actual parser.
11. Known Incomplete Definitions¶
This initial grammar is a starting definition, not yet a complete normative grammar.
The following areas require further specification:
- Exact numeric literal formats.
- String and character escaping.
- Complete operator list and precedence.
- List, map, tuple, optional, and Result syntax.
- Reference and borrowing syntax.
- Asynchronous and parallel execution syntax.
- Complete loop and MATCH grammar.
- Error and recovery syntax.
- Module visibility details.
- Exact block and statement termination rules.
These definitions must be completed before the grammar can be considered implementation-ready.
12. Design Goal¶
Every valid program must have a precise syntactic definition.
AI agents must be able to generate source code that follows deterministic grammar rules, while the compiler must reject malformed or unsupported syntax without guessing at the intended meaning.
Source and related sections¶
Source file: TECHSPEC-20.md (preserved in source-original/LANG/). See the specification index, the glossary, and the cross-reference index.