#65 TLA+, Quint and Formal Verification in the Age of AI - Gabriela Moreira - Type Theory Forall

Om avsnittet

How can we be sure that our code is doing what is supposed to be doing?

And this is the role of formal verification at large: A Discipline to trust that the code is doing what it is supposed to do.

In this episode I talk with Gabriela Moreira, the CEO of Quint. A Specification Language spun out of TLA+ designed to help us deeply understand that our code is doing what it is supposed to be doing.

We talk about the story behind Quint, it’s relationship with TLA+, how does it compare with other specification languages such as Alloy. We get into the details of different flavors of logic, such as Modal and Temporal Logic. We also talk briefly about teaching these tools to undergrads, and the great role that they may take in the era of AI generated code.

#65 TLA+, Quint and Formal Verification in the Age of AI - Gabriela Moreira

Om avsnittet

Links

Fler avsnitt

#64 PL Education in the Age of AI - Shriram Krishnamurthi

#63 Hack: Typing PHP at Facebook Scale - Julien Verlaguet

#62 Dependent Haskell - Vladislav Zavialov

#61 Zurihac Behind the Scenes - Farhad Mehta

#60 Conversations on Life, AI, and the PL Job Market - Pedro and Dan

#59 Category Theory and Inclusivity - Valeria de Paiva

#58 Constructivism and Computational Content - Andrej Bauer

#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik

#56 Property Based Testing and PL Grad School Applications - Francille Zhuang

#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber