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
All contributions to the show are greatly appreciated!
- Patreon
- Ko-Fi (one-off)
- BTC : bc1qsqccnk0f02tue6jkch72v0z990r2rwv6mdgu9y5f5jgdu9ux69yq6slfy2
