People often ask us: what is type theory and why is it useful? Type Theory is the academic study of type systems: formal frameworks for classifying terms, structuring computation, and specifying the behavior of programs. It investigates how types enforce invariants, guarantee safety properties, and shape the design of programming languages. Its impact is both theoretical and practical. 1) Programming language design and metatheory Type theory provides the tools to state and prove properties such as type safety, normalization, and parametricity. These results are not testing heuristics. They are mathematical guarantees. As Dijkstra wrote, “Program testing can be used to show the presence of bugs, but never to show their absence.” Tests explore a finite search space. Proofs quantify over infinite domains. Type theory is the foundation that makes such proofs possible in programming language research. 2) Industrial impact: Rust and RustBelt Careful type theoretic design eliminates entire classes of bugs at compile time. The RustBelt project went further and formally verified core aspects of Rust’s type system using the Rocq proof assistant, with peer reviewed results in top PL venues. This is not marketing. It is mechanized metatheory. 3) Proof assistants and formal verification Type theory is the theoretical backbone of systems such as Lean, Rocq, Agda, and also HOL based systems such as Isabelle/HOL. These are programmable logics where specifications and proofs coexist with code. In an era of AI assisted development, proof assistants offer a different paradigm. Instead of generating plausible text, we iteratively construct machine checked proofs against a formal specification. The result is not just confidence. It is correctness by construction. For students and engineers working on compilers, DSLs, or formal methods, type theory is not an abstract curiosity. It is the language in which we make precise claims about programs and then prove them. If you are interested in learning more about type theory, programming languages, and proof assistants, follow us here and subscribe on Youtube: piped.video/@typetheoryforal….

Interested in a PhD studentship in the Functional Programming Lab in Nottingham? Fully-funded studentships are currently being advertised; deadline 6 January 2027. Please share, and encourage excellent students to apply! people.cs.nott.ac.uk/pszgmh/…

linear logic is interesting. it captures the fact that some arguments can only be used once, e.g. you can’t skip out on work claiming your grandmother died more than twice

FP folks -- please encourage recently completed PhD students to publish their dissertation abstracts in the Journal of Functional Programming: simple process, no refereeing, open access, 250+ published to date, deadline 30th November 2026. Please share! tinyurl.com/jfp-phd-abstract…

The current focus on correctness is exciting, but claiming “X is formally verified” says little on its own. You need to specify which properties were verified and under what assumptions. Formal verification is not a blanket guarantee of correctness! For example, here are some proofs about Erlang's json module using the Lynx project: github.com/josevalim/lynx/bl… It would be imprecise to say "Erlang's json is formally verified". However, I can say that Erlang's json encoding and decoding have been proved to round trip for integers, floats, booleans, null, UTF-8 strings, lists and maps with UTF-8 string keys of them, nested at most 64 deep.

Now that I've landed my dream FV job I've written a blog post explaining how I used Claude+Notion to help me keep track of the job applications. Maybe some other people may also find this useful: pedroabreu0.github.io/blog/2…

Happy to announce that our FV Job Board now has a RSS 2.0 feed! Now you can follow the newest job updates through your favorite RSS feed reader. typetheoryforall.github.io/F… As always, this is a community project and job updates and PRs are very welcome!

Excited to see what will come out of this!

Just published a comprehensive behind the scenes of our this formal verification job search in our Patreon patreon.com/TypeTheoryForall…

Happy to announce that we've just found and added 150 Formal Verification roles across the globe to our website: typetheoryforall.github.io/F… Contributions are always welcome! I'm not sure if I like the current layout, so if you have other ideas, feel free to open an issue to discuss

We have an actual website for FVjobs! typetheoryforall.github.io/F… Thanks @OndraLengal for the PR! Other PRs for better functionality and usability are very welcome! If you know of open Formal Verification Jobs please add them through this form: github.com/typetheoryforall/…

Formal verification has been getting a lot of attention lately, so we decided to put together FVjobs, a community-maintained job board to keep track of who's actually hiring. For now, GitHub and GitHub Issues should be enough. Depending on how things develop, we might eventually build a proper website. Contributions are greatly appreciated! No GitHub knowledge is necessary. If you know of an open position, you can simply fill out this form: github.com/typetheoryforall/… Issues and PRs are also very welcome! github.com/typetheoryforall/…

Wonder why none of the people in formally verified software are having a meltdown right now? Answer: Because it was obvious to any expert that superhuman AI would be a prerequisite to really writing formally verified software with dependent types.

More speed, more check marks, more formal verification. None of it matters without understanding. Catch the whole conversation with @bugarela on @ttforall.

How on earth has this masterpiece been around since 2021 and I'm only seeing this now??? @RanjitJhala piped.video/Ci48kqp11F8?is=i7e0…

New TTFA episode is out! 🎙️ This time I sat down with Gabriella Mora, CEO of Quint, to talk about formal specifications, TLA+, temporal logic, and the increasingly important role of formal methods in the age of AI. With AI generating more and more code, how can we make sure that the software we're building actually behaves as intended? We also discuss the story behind Quint, how it compares to Alloy, and the challenges of teaching formal methods. I think this is a particularly timely conversation given everything happening at the intersection of AI and formal verification. 0:00 Intro 2:10 Gabriela's path: from Tumblr themes to a TLA+ thesis 11:56 Quint and TLA+ vs. Alloy 15:05 Why write a spec? Understanding over checkmarks 22:04 How AI changes the economics of formal methods 27:19 Executable specs as the middle ground for AI-written code 36:13 Keeping spec and code in sync: codegen, model-based testing, trace validation 39:04 Inside Quint Studio 47:53 Quint vs. TLA+: syntax, types, effects and the simulator 54:08 Model checking: a new Rust checker, TLC and Apalache 1:02:31 Temporal logic: modal operators, LTL vs. CTL 1:07:41 In practice: invariants, witnesses and cheap liveness checks 1:12:33 Bugs found in audits just by writing the spec 1:16:13 From Informal Systems and blockchain to Quint 1:23:38 Spinning Quint out and becoming CEO 1:36:19 Teaching formal methods as AI learned to write Quint 1:41:12 Teaching with games, and what students found hardest 1:50:56 What's next for Quint and Quint Studio 1:57:44 Wrap-up and outro

New TTFA episode! 🎙️ I sat down with @bugarela, CEO of Quint, to discuss formal specifications, TLA+, temporal logic, and how formal methods can help us trust AI-generated software. We also explore the story behind Quint, its comparison with Alloy, and the challenges of teaching formal methods in the age of AI. A timely conversation about where software engineering is heading! piped.video/SdwjRJgp6gs

SMT timeouts, unknown results, or trust concerns? SMTLib-to-Lean4 translates SMT-LIB queries into well-typed Lean 4 code! GitHub: github.com/LeanHorn/SMTLib-t… Inspired by earlier work on Lean 4 backend for Flux: arxiv.org/pdf/2607.12226 In collab with @RanjitJhala