Thales – TypeScript compiler and JavaScript engine in Lean

Thales A TypeScript-to-Lean 4 compiler. Thales type-checks a safe subset of TypeScript and emits a Lean 4 sidecar alongside the input .ts file, turning your TypeScript module into a Lean module you can reason about. Thales sits on top of strict TypeScript. Every program Thales accepts is also accepted by tsc --strict — we don't invent new syntax or reinterpret existing type rules, so your editor tooling, IDE integrations, and CI linters keep working. What Thales does is further restrict TS (rejecting mutation, classes, async, untyped escapes, etc.) and enrich selected patterns — nullable unions, @throws, @total — with Lean-visible semantics that TypeScript's own type system cannot express. The result: a narrow, disciplined subset of TS whose emitted Lean you can actually reason about.

…

Excerpt limited to ~120 words for fair-use compliance. The full article is at GitHub.