Kodsnack26 Nov 2024

Kodsnack 612 - Where types first come in, with Pedro Abreu

Fredrik talks to Pedro Abreu about the magical world of type theory. What is it, and why is it useful to know about and be inspired by?

Pedro gives us some background on type theory, and then we talk about how type theory can provide new ways of reasoning about programs, and tools beyond tests to verify program correctness. This doesn't mean that all languages should strive for the nirvana of dependent types, but knowing the tools are out there can come in handy even if the code you write is loosely typed.

We wrap up with some further podcast tips, of course including Pedro's own podcast Type theory forall.

Thank you Cloudnet for sponsoring our VPS!

Comments, questions or tips? We a re @kodsnack, @tobiashieta, @oferlundand @bjoreman on Twitter, have a page on Facebook and can be emailed at info@kodsnack.se if you want to write longer. We read everything we receive.

If you enjoy Kodsnack we would love a review in iTunes! You can also support the podcast by buying us a coffee (or two!) through Ko-fi.

Links

Pedro
Type theory
Type theory forall - Pedro's podcast
Chalmers
The meetup group through which Pedro and Fredrik met
Purdue university
Bertrand Russell
The problem of self reference
Types
Set theory
Kurt Gödel
Halting problem
Alan Turing
Turing machine
Alonzo Church
Lambda calculus
Rust
Dependent types
Formal methods
Liquid types - Haskell extension
SAT solver
Property-based testing
Quickcheck
Curry-Howard isomorphism
Support Kodsnack on Ko-fi!
Functional programming
Imperative programming
Object-oriented programming
Monads
Monad transformers
Lenses
Interactive theorem provers
Isabelle
HOL
Dafny
Saul
Crucible
Symbolic execution
CVC3, CVC5 solvers
Pure functions
C#
Algebraic data types
Pattern matching
Scala
Recursion
Type theory forall episode 17: the first fantastic one with Conal Elliot. The discussion continues in episode 21
Denotational types
Coq
IRC
Software foundations - about Coq and a lot more
The church of logic podcast
The Iowa type theory commute podcast

Titles

Type theory podcasts
Very odd for some people
Brazilian weather
Relearning to appreciate
The dawn of computer science
Layers of sets
Where types first come in
Bundle values together
The research about programming languages
If you squint your eyes enough
Nirvana of type systems
Proofs all the way down
Extra guarantees
If your domain is infinite
Formal guarantees
The properties of my system
What is the meaning of my program?
Building better systems

Det här avsnittet är hämtat från ett öppet RSS-flöde och publiceras inte av Podme. Det kan innehålla reklam.

Avsnitt(715)

Kodsnack 701 - The chicken would explode, with Holly Cummins

Fredrik chats to Holly Cummins about using Minecraft for observability, other amazing Quarkus tricks, and the value of joy at work. Recorded during Øredev 2025. Thank you Cloudnet for sponsoring our V...

5 Maj 38min

Kodsnack 700 - Varför har vi så bråttom?, med Benny Andrén och Markus Borg

Fredrik snackar med Benny Andrén och Markus Borg om AI-drivet återupptäckande av sunda arbetssätt. Benny har börjat fundera över vilka problem AI egentligen löser, och om våra försök att tämja modelle...

26 Apr 42min

Kodsnack 699 - A two-IDE person, with Shawn Wildermuth

Fredrik chats to Shawn Wildermuth about evolving in the world of software development, small changes adding up, developer hiring, not chasing the new thing, and quite a bit more. Fredrik is still hopi...

21 Apr 42min

Kodsnack 698 - Man ställer frågan noll, med Petter Ericson

Fredrik snackar problem med AI med Petter Ericson, forskare på Umeå universitets AI policy lab. Det finns så mycket fler diskussioner och frågetecken kring AI än att bara om en språkmodell kan göra en...

14 Apr 53min

Kodsnack 697 - En djefla man som flyttar många jiror

Fredrik snackar med Bartek Tatkowski om livs- och arbetsfilosofi knappt halvvägs in i en utvecklarkarriär. Det var ju vi som skulle frambringa den bättre framtiden! Sedan kom 2025. 2025 var ett konsti...

7 Apr 43min

Kodsnack 696 - Gramse

Fredrik och Kristoffer snackar om Gram, Kristoffers avskalade fork av Zed. Det började - som det så ofta gör - med en jakt på en vettig kodredigerare för nybörjare och ett orimligt licensavtal. Sedan ...

31 Mars 54min

Kodsnack 695 - Programmet lär inte ut någonting, med Göran Hjalmarsson

Fredrik snackar med Göran Hjalmarsson, mannen bakom det klassiska mattespelet Cheops pyramid och Alega software. Göran berättar Alegas och Cheops historia - från starten med ställbara stjärnkartor och...

24 Mars 40min

Kodsnack 694 - Dark patterns … to rule them all, with Sergès Goma

Fredrik chats to Sergès Goma about dark patterns and her Øredev presentation on them. We start off by talking about giving presentations and the background to the dark patterns talk. All the great ver...

17 Mars 31min