Jesse Alama

A longer-term aim is to complete the deep embedding of TypeScript into Lean (which will coexist alongside the current shallow embedding), enabling features such as LSP integration and an MCP server to help harden TS programs with AI assistance.

Currently, we support JSDoc-style assertions such as `@total`, `@pure` to express the totality (program terminates on all arguments without exceptions) and purity (no mutation) of JS functions. But that's just the tip of the iceberg. More assertions and program properties coming!

I'm happy to announce Thales, a TypeScript compiler and JS engine in Lean. Thales compiles a subset of TypeScript to Lean via a shallow embedding. I'm building a bridge for TS programmers into Lean's program verification toolset. Check out github.com/jessealama/tha… to get started.