Episode 4: Formally Verifying Your Taxes With Catala!
Formal verification has been used to prove the security of
cryptographic protocols like Signal and TLS – but can it also be
used to verify the correctness of legislation? Denis Merigoux tells
us about how Catala wants to use formal methods to verify the
F
44 Minuten
Podcast
Podcaster
In-depth, substantive discussions on the latest news and research in applied cryptography.
Beschreibung
vor 5 Jahren
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.
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.
Weitere Episoden
49 Minuten
vor 2 Jahren
53 Minuten
vor 2 Jahren
52 Minuten
vor 2 Jahren
47 Minuten
vor 4 Jahren
43 Minuten
vor 4 Jahren
In Podcasts werben
Kommentare (0)