« All posts

Introducing Thales: TypeScript Compiler and JavaScript Engine

Thales is a compiler that converts TypeScript to Lean 4 modules, promoting safer code practices.

Thales is a compiler that type-checks a safe subset of TypeScript and emits a Lean 4 sidecar. This tool transforms TypeScript modules into Lean modules, enabling engineers to write safer and more reasoned code. By rejecting features like classes and async, Thales enriches TypeScript semantics with Lean-compatible constructs.