Type Theory Forall

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.

Links

Gabriela's Website

Quint's Website

Quint Studio Waitlist

All contributions to the show are greatly appreciated!

Patreon

Ko-Fi (one-off)

BTC : bc1qsqccnk0f02tue6jkch72v0z990r2rwv6mdgu9y5f5jgdu9ux69yq6slfy2

Shriram has devoted his Career to advance the teaching of programming of programming languages. he is a professor at Brown, The author / co-author of different books about this, and a major contributor the Racket Programming Language.

In this episode we talk in depth about why PL education is so important, what can students really gain from in practice? What is changes in the age of AI? Is programming even going to be a thing in the years to come!?

All contributions to the show are greatly appreciated!

Patreon

Ko-Fi (one-off)

BTC : bc1qsqccnk0f02tue6jkch72v0z990r2rwv6mdgu9y5f5jgdu9ux69yq6slfy2

Links

Shiriram's Website

Shriram's Twitter

On the Expressive Power of Programming Languages PWL'2019 talk

Julien is one of the creators of Hack, a language developed by Facebook to introduce types into PHP. In this episode he talks in depth about the semantics of PHP, and all the ways that it is inhenrently broken, process of development of Hack, the design decisions, the kind of guarantees that could be enforced to PHP and that developers should care about.

This episode was brought to you by SkipLabs: Julien’s company to make reactive programming robust and seamless!

Links

SkipLabs

Computers Coffee and Beer

Julien's Website

Julien's Linkedin

All contributions to the show are greatly appreciated!

Patreon

Ko-Fi (one-off)

BTC : bc1qsqccnk0f02tue6jkch72v0z990r2rwv6mdgu9y5f5jgdu9ux69yq6slfy2

Vlad works at Serokell to develop the Glasgow Haskell Compiler, he is a former member of the Haskell Steering Committee and the current implementer of Dependent Haskell.

In this conversation we talk about the development process of the GHC, he explains with detail how’s the decision process of the community to modify the language through the Haskell Steering Committee. And we get pretty technical discussing the GHC internals, he basically gives us a class of how things looks like and how can a newcomer start hacking the GHC today.

And of course, we go into details of the theory and implementation of Dependent Haskell!

Links

Serokell
Serokell on X
Vlad on X
Dependent Haskell Roadmap

All contributions to the show are greatly appreciated!

Patreon

Ko-Fi (one-off)

BTC : bc1qsqccnk0f02tue6jkch72v0z990r2rwv6mdgu9y5f5jgdu9ux69yq6slfy2

In this episode we talk with Farhad Mehta, one of the main organizers of Zurihac, the biggest Haskell event in the planet.

Zurihac happens once a year at Zurich. This year’s Zurihac will be on june 6, 7 and 8.

Links

Zurihac Website

Types Discussion on the use of AI

Agda Discussion on the use of AI

All contributions to the show are greatly appreciated!

Patreon

Ko-Fi (one-off)

BTC : bc1qsqccnk0f02tue6jkch72v0z990r2rwv6mdgu9y5f5jgdu9ux69yq6slfy2