Aether Formal Core

The proof-facing core of Aether-Lang for Lean 4: the executable subset shared by the parser, interpreter, and Titan VM. Theory →

Lexical Surface

Token	Accepted forms
Identifiers	ASCII identifiers for variables, parameters, functions
Numbers	integer literals; fixed micro-precision decimal floats (1.5)
Booleans / unit	true, false; unit
Strings	escapes \", \\, \n, \r, \t
Comments	// line; nestable /* */ block; unterminated block = lexer error
Lists	[...] of core expressions; newlines between elements; trailing comma before ]
Separators	newline (LF, CRLF or CR), ~, ;
Range	.. — 1..10 lexes as Number(1), DotDot, Number(10)
Seal alias	seal and 🦭 are the same keyword
Operators	+ - * / % == != < > <= >= && \|\| !

Theory →

Core Syntax

program  ::= stmt*

stmt     ::= "let" ident (":" ann-ty)? "=" newline* expr
           | ident "=" newline* expr
           | "if" newline* expr block ("else" block)?
           | "while" newline* expr block
           | "for" ident "in" signed-int ".." signed-int block
           | "seal" ("until" newline* expr)? block
           | "fn" ident newline* "(" params? ")" (":" ann-ty)? block
           | "return" expr?
           | "break"
           | "continue"
           | expr

block    ::= separator* "{" stmt* "}"
separator ::= newline | "~" | ";"
params   ::= ident ("," newline* ident)* ","? newline*
           | ident ":" ann-ty ("," newline* ident ":" ann-ty)* ","? newline*
ann-ty   ::= "num" | "bool" | "str" | "unit"
           | "list" "[" newline* ann-ty newline* "]"

expr     ::= literal
           | ident
           | ident newline* "(" call-args? ")"
           | "[" list-items? "]"
           | "(" newline* expr newline* ")"
           | expr "[" newline* expr newline* "]"
           | expr "." newline* ident
           | expr "." newline* ident "(" call-args? ")"
           | "-" newline* expr
           | "!" newline* expr
           | expr binop newline* expr

call-args ::= arg ("," newline* arg)* ","? newline*
arg      ::= expr | ident "=" expr
list-items ::= expr ("," newline* expr)* ","? newline*
binop    ::= "+" | "-" | "*" | "/" | "%"
           | "==" | "!=" | "<" | ">" | "<=" | ">="
           | "&&" | "||"
literal  ::= number | float | bool | string | unit
signed-int ::= number | "-" number

Precedence (low → high)	Operators
1	\|\|
2	&&
3	==, !=
4	<, >, <=, >=
5	..
6	+, -
7	*, /, %
8	unary -, !
9	postfix expr[expr], expr.ident, expr.ident(args?)
10	primary expressions

Runtime Values

Value ::= Num int | Float int micros | Bool bool | Str string | List Value* | Unit
Flow  ::= Value Value | Return Value | Break | Continue

Host values (manifolds, classes, tensors, native functions) sit outside the core. Theory →

Statement Semantics

Execution maps an environment and a statement to a flow. Theory →

Value	Truthy?
Bool(false), Num(0.0)	false
empty string, empty list	false
Unit, unsupported values	false
other booleans, nonzero numbers, non-empty strings and lists	true

Static Typing

Types: num, bool, str, unit, list[T], unknown; unknown is accepted wherever a concrete type is still imprecise. Theory →

Target	Field / pure method	Result
str, list	.length, .len()	num
str, list	.is_empty()	bool
str	.first(), .last(), .tail(), .reverse(), .at(i), .take(n), .drop(n)	str
str	.contains(s), .starts_with(s), .ends_with(s)	bool
list[T]	.first(), .last(), .at(i)	T
list[T]	.tail(), .reverse(), .take(n), .drop(n), .append(v), .prepend(v), .concat(xs)	list[T]
list[str]	.join(sep)	str
list[T]	.contains(v)	bool

Bytecode Correspondence

Construct	Bytecode
Numeric / boolean / unit constants	PUSH, PUSH_BOOL, PUSH Unit
Locals	LOAD, STORE
Arithmetic and logic	ADD SUB MUL DIV MOD NEG EQ NEQ LT GT LE GE AND OR NOT
Lists, strings, fields, methods	list construction, indexing, .length, every pure method in the table above
Branching	JMP, JMP_IF_FALSE
break / continue	patched JMP to loop exit / continuation
Functions	CALL(target, arity), RET
Program end	HALT

First VM proof target: compiler output for a well-formed program never underflows the stack. Theory →

Current Boundaries

Not yet in the formal core:

• Classes, methods, object creation, modules, imports.
• Manifold, block, render, regress, topology-specific host operations.
• Named function arguments in user-defined calls.
• General object/class field access beyond proof-core .length.
• Mutating or host/object method calls beyond proof-core pure .len().
• Tensor and ML model handles.
• Forward function references before declaration in VM lowering.
• Global variable capture inside VM user functions.

Lean 4 Formalization

lake build

File	Contents	Theory
lakefile.lean	Lake package aether-formal
lean-toolchain	Lean toolchain pin
Aether.lean	top-level import
Aether/Lexer.lean	token kinds, tokenize, tokenizeLocated with SourceSpan	→
Aether/Parser.lean	token-to-core parser, parseProgramDetailed	→
Aether/Static.lean	well-formedness and type checking, checkProgramDetailed	→
Aether/Core.lean	syntax, values, envs, eval, StepStmt/StepBlock, FnEnv relations	→, →, →
Aether/VM.lean	stack VM, frame VM, compileCheckedFrameProgram	→, →
Aether/Pipeline.lean	stage-aware lex/parse/static/compile/runtime diagnostics	→

Executable Witnesses

Each witness checks a Prop-level fact against the bounded executor on a concrete example. Theory →

Checked Compilation

A successful checked compile implies the static checker accepted the source. Theory →