36 min listen
Episode 4: Formally Verifying Your Taxes With Catala!
FromCryptography FM
ratings:
Length:
44 minutes
Released:
Oct 20, 2020
Format:
Podcast episode
Description
Anyone who’s looked at the French civil code -- or, God forbid, the French tax code -- will tell you that it takes more than a mere human mind to decipher its meaning, given how it’s been growing and growing ever since it was established by Napoleon hundreds of years ago.
Well, Catala is a new project that takes this adage perhaps a bit too literally, by applying formal methods -- a field increasingly seen as immediately adjacent to cryptography -- on the French tax code! Catala aims to provide a “domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts.” -- what that means is that you’ll be able to describe the tax code in a programming language, and get a proven-correct processing of your tax returns in that same language, too!
This episode of Cryptography FM is not directly about cryptography. Instead we’ll be covering a highly related and definitely interesting tangent: can we use the same formal methods that have recently proven the security of protocols like Signal and TLS in order to formally verify our tax returns? And, more importantly, can today’s guest help me pay less taxes?!
Joining us today is doctoral student Denis Merigoux, to talk about Catala, and more.
Links:
* Catala homepage (https://catala-lang.org/)
Music composed by Toby Fox and performed by Sean Schafianski (https://seanschafianski.bandcamp.com/). Special Guest: Denis Merigoux.
Well, Catala is a new project that takes this adage perhaps a bit too literally, by applying formal methods -- a field increasingly seen as immediately adjacent to cryptography -- on the French tax code! Catala aims to provide a “domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts.” -- what that means is that you’ll be able to describe the tax code in a programming language, and get a proven-correct processing of your tax returns in that same language, too!
This episode of Cryptography FM is not directly about cryptography. Instead we’ll be covering a highly related and definitely interesting tangent: can we use the same formal methods that have recently proven the security of protocols like Signal and TLS in order to formally verify our tax returns? And, more importantly, can today’s guest help me pay less taxes?!
Joining us today is doctoral student Denis Merigoux, to talk about Catala, and more.
Links:
* Catala homepage (https://catala-lang.org/)
Music composed by Toby Fox and performed by Sean Schafianski (https://seanschafianski.bandcamp.com/). Special Guest: Denis Merigoux.
Released:
Oct 20, 2020
Format:
Podcast episode
Titles in the series (24)
Episode 1: Post-Quantum TLS With KEMs Instead of Signatures!: KEMTLS is a modified version of TLS 1.3 that uses Key Encapsulation Mechanisms, or KEMs, instead of signatures for server authentication, thereby providing a sort of “post-quantum TLS”. But what even are KEMs? Are quantum computers even a thing that we should be worried about? On the first ever episode of Cryptography FM, we’ll be hosting Dr. Douglas Stebila and PhD Candidate Thom Wiggers to discuss these questions and more. by Cryptography FM