Type Theory Forall

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: youtube.com/@typetheoryforal….

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/…

How on earth has this masterpiece been around since 2021 and I'm only seeing this now??? @RanjitJhala youtu.be/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! youtu.be/SdwjRJgp6gs

Clément was awarded the best teaching award from EPFL’s School of Computer and Communication Sciences Very well deserved. Zero surprises! He is one of the most curious and enthusiastic researchers I had the pleasure to meet. Congratulations Clément!! Btw the invitation to com chat at ttfa is always open for you! :)

Now this is good use of AI for marketing

I certainly really hope for this. In fact just had a conversation with @bugarela exactly about that, I'll try to release that asap.

Please show your FV ID card at the entry desk before tagging me please. Thank you. For those who don't have an FV ID card please get in touch with @typememetics, they're in charge with personnel profiling.