@alamajamn
Joined February 2026
  • Tweets21
  • Following20
  • Followers15
I'm happy to announce pabst: a tool for Property-Based Testing in TypeScript. Annotate your functions with properties they're supposed to have, run `pabst test` to try to invalidate those claims, and watch the bugs come flying out!. Install via `npm install pabst-checker`,
1
3
26
Pabst arose from a session at Igalia's Web Engines Hackfest, entitled "Beyond testing and type-checking JavaScript: Can we be bothered?" We were lucky to have Nicolas Dubien, of fast-check (fast-check.dev/ ), with us. Pabst is essentially just a front-end to fast-check.

fast-check official documentation | fast-check

fast-check is a Property-based Testing framework for JavaScript and TypeScript. It works with Jest, Mocha, Vitest, and others. Let's fuzz!

fast-check.dev
1
10
Pabst helped me find several bugs in my polyfills for the TC39 Decimal and Amount proposals, which had 100% test coverage.
1
8
Jesse Alama retweeted
Lean
@leanproverMar 25
Interested in Lean and near 🇫🇷 Paris? The inaugural Paris Lean Meetup is happening April 24 at 7:00 PM, hosted by Mistral AI. Two talks: Leonardo de Moura of Lean FRO, and the Mistral team introducing Leanstral, their open-source code agent for Lean 4. Pizza and informal discussion afterward. 🔗 Registration details here: meetup.com/lean-paris/events…
4
16
6
160
13,078
Jesse Alama retweeted
Anil Madhavapeddy
@avsmJun 11
Jane Street is turning into a Lean, Clean, Rocq-and-roll theorem machine!
Yaron (Ron) Minsky
@yminskyJun 11
I've been telling people for 25 years that Jane Street is not interested in formal methods. No more! And we're actively hiring to form a new formal methods team!
1
12
112
10,079
Watching Terence Tao's cleanup of a Lean proof to meet Mathlib guidelines, I'm struck by the problem we're in of there being too much math. There are so many good Lean proofs but essentially only one blessed outlet for them. "MathOverflow" indeed! youtube.com/watch?v=l3SCK6V-…
2
47
I'm in Tsukuba, Japan for FLOPS 2026! After last week's Formal Methods symposium, this will be another packed week of learning. I'll be presenting a tutorial on Lean, extracted from my TypeScript-to-Lean compiler. functional-logic.org/events/…

Symposium on Functional and Logic Programming 2026 | Functional Logic Programming

18th International Symposium on Functional and Logic Programming

functional-logic.org
1
29
Getting ready to attend day 1 of AI, Proof and Verification (AIPV) at Formal Methods 2026 in Tokyo. aipvconf.org/

AIPV2026

Colocated with FM2026 in Tokyo

aipvconf.org
1
25
I'm on my way to Japan to attend Formal Methods. The agenda is absolutely packed with great stuff; really excited to learn a ton. It'll be my first time at FM. If you're interested in Lean & program verification, let's talk! conf.researchr.org/home/fm-2…
15
Jesse Alama retweeted
Paulo Matos
@pocmatosMay 12
Like a lot of people, when agents could code I didn't double my projects. I 15x'd them. Then I got lost. So I built pewpew, a canvas for tracking them all. It made me suspect the IDE is the wrong shape. p.ocmatos.com/blog/pewpew-th… #AgenticCoding #ClaudeCode #Codex

Pewpew: the terminals are down! - Notes & Code

Fifteen Ghostty terminals, one canvas, and the suspicion that the IDE is the wrong shape for the agentic era.

p.ocmatos.com
1
1
54
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/thales to get started.

GitHub - jessealama/thales: TypeScript compiler and JavaScript engine in Lean

TypeScript compiler and JavaScript engine in Lean. Contribute to jessealama/thales development by creating an account on GitHub.

github.com
3
17
1
69
6,511
more replies
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!
1
3
155
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.
3
127
Load more