Kodsnack26 Marras 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

Tämä jakso on lisätty Podme-palveluun avoimen RSS-syötteen kautta eikä se ole Podmen omaa tuotantoa. Siksi jakso saattaa sisältää mainontaa.

Jaksot(715)

Kodsnack 677 - It's all quantum, with Natalia Chepiga

Recorded on-stage at Øredev 2025, Fredrik talks to Natalia Chepiga about quantum computing and where you, personally, might see it first. We need classical computers to make quantum computers better. ...

4 Joulu 202511min

Kodsnack 676 - Maps will get you fired, with Simon Wardley

Recorded on-stage at Øredev 2025, Fredrik talks to Simon Wardley about maps (not the same as charts!), stories, commodotization, digital sovereignty, getting labeled a heretic by all sides, and a lot ...

4 Joulu 202526min

Kodsnack 675 - Curate the world, with Nicklas Hermansson

Recorded on-stage at Øredev 2025, Fredrik talks to Sweden's foremost trend spotter Nicklas Hermansson about how you become a futurist. From how Nicklas got there, what his days look like, and how he c...

4 Joulu 202514min

Kodsnack 674 - Make the visions louder, with Tiera Fletcher

Recorded on-stage at Øredev 2025, Fredrik talks to Tiera Fletcher about her lightning tour of going to Mars and what might happen on the way. And also about - for example - finding visions to guide yo...

4 Joulu 202519min

Kodsnack 673 - Ett mönster för allt

Fredrik och Kristoffer snackar musik, böcker, och kodstädande. Kristoffer överväger ett hus, som tillbehör till sina trummor. Efter att ha avhandlat bra ljud på olika sätt diskuterar vi böcker och hur...

2 Joulu 202547min

Kodsnack 672 - Inte bloata binären

Fredrik, Kristoffer, och Tobias snackar om Tobias snart avslutade tid på Ubisoft och vad som händer därefter. Tobias diskuterar bland annat vad han lärt sig under fyra år på en stor studio. Vad har ha...

25 Marras 20251h 2min

Kodsnack 671 - Alla abstraktioner hela tiden, med Andreas Ekeroot

Fredrik snackar med Andreas Ekeroot (mannen från avsnitt 603!) om abstraktioner, Ash, och annat. Vi börjar med att diskutera abstraktioner lite mer allmänt, från filsystem via abstraktioner i språket ...

18 Marras 20251h 8min

Kodsnack 670 - Prat om paradigm, med Daniel Raniz Raneland och Johan Thelin

Fredrik snackar med först Johan Thelin och sedan Daniel Raniz Raneland om paradigm, och om konferensen Lindholmen software development day som alla tre nyss deltagit i. Konferensen firade tjugo år oc...

11 Marras 20251h 6min