Logic & Formal Methods Videos Hacker News Recommends
Logic & formal methods videos on HackerTube: the talks, lectures and explainers Hacker News commenters keep sharing, covering proof assistants, Coq, Lean, TLA+, type theory and proofs, SAT solvers, model checking, program correctness, foundations of mathematics, set theory.
32 videos · ranked by HN recommendations
Most recommended logic & formal methods videos
The ones HN returns to most often when a thread turns to this topic.
lecture#162Brian Beckman: Don't fear the Monad
jasonofthel33t
“This video is all you, as a practicing programmer, need to know about monads and it's just 1 hour long.”
9 HN recommenders · 2012–2024
talk#20328c3: The Science of Insecurity
28c3
“The best talk on computer security I have seen is Meredith Patterson's Science of Insecurity at 28c3”
9 HN recommenders · 2012–2024
talk#212"Propositions as Types" by Philip Wadler
Strange Loop Conference
“best ~40 minutes I've ever spent.”
9 HN recommenders · 2015–2026
explainer#399Math's Fundamental Flaw
Veritasium
“I found Veritaseum's video about it really clear and instructive”
7 HN recommenders · 2021–2024
explainer#425The Banach–Tarski Paradox
Vsauce
“This vsauce video is actually a really accurate (and entertaining!) introduction to set theory”
6 HN recommenders · 2015–2024
talk#456The Future of Mathematics?
Microsoft Research
“For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN.”
9 HN recommenders · 2019–2025
talk#714Leslie Lamport: Thinking Above the Code
Microsoft Research
“He's just saying that you should think before you code and that most specifications should be just a few sentences stating what you intend to do.”
5 HN recommenders · 2015–2026
explainer#773How To Count Past Infinity
Vsauce
“The most accessible resource I found was this VSauce video”
6 HN recommenders · 2016–2022
talk#883"Finding bugs without running or even looking at code" by Jay Parlar
Strange Loop Conference
“There is a talk that gives a good overview on Alloy and how useful using something like this is”
4 HN recommenders · 2019–2023
talk#1032Edwin Brady - Idris 2 - Type-driven Development of Idris
Curry On!
“Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action.”
4 HN recommenders · 2019–2023
explainer#1124Infinity is bigger than you think - Numberphile
Numberphile
“Numberphile did a pretty good introductory video to this if you want to learn more”
3 HN recommenders · 2014–2022
talk#12162017 ACM PPoPP Keynote: It's Time for a New Old Language
Guy Steele
“an excellent talk by Guy Steele that goes over issue of notation and balkanization”
3 HN recommenders · 2018–2023
talk#1397Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18
Code Sync
“this looks like a good introduction”
5 HN recommenders · 2018–2024
talk#1457"A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram
Strange Loop Conference
“I recommend watching this presentation for a good idea of what ATS programming is like”
4 HN recommenders · 2017–2022
talk#1616Hillel Wayne - Beyond Unit Tests: Taking Your Testing to the Next Level - PyCon 2018
PyCon 2018
“I found this talk (by the same person being interviewed) to be concise and convincing on how to do better than typical practice”
3 HN recommenders · 2018–2023
lecture#2031Lec 1 | MIT 6.042J Mathematics for Computer Science, Fall 2010
MIT OpenCourseWare
“the professor tells relatable stories to motivate the new concepts”
3 HN recommenders · 2017–2018
lecture#2055What if Current Foundations of Mathematics are Inconsistent? | Vladimir Voevodsky
Institute for Advanced Study
“I recommend this video”
3 HN recommenders · 2017–2019
talk#2149"Tackling Concurrency Bugs with TLA+" by Hillel Wayne
Strange Loop Conference
“If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk.”
3 HN recommenders · 2018–2025
lecture#2228MIT Godel Escher Bach Lecture 1
jasonofthel33t
“They’re great to watch as you work through the book”
3 HN recommenders · 2017–2021
tutorial#2398A Tour of Prolog
The Power of Prolog
“check out this video introduction by Markus Triska about what makes Prolog unique”
2 HN recommenders · 2022–2024
talk#2561Philip Wadler - Propositions as Types (Lambda Days 2016)
Erlang Solutions
“This is a very good lecture series[4].”
2 HN recommenders · 2016–2021
talk#2585Barliman: trying the halting problem backwards, blindfolded - William Byrd, Greg Rosenblatt
ClojureTV
“I work on miniKanren, which is a logic programming language with a complete search that doesn't hit the nontermination issues you mention.”
3 HN recommenders · 2017–2024
talk#2960"Type-Driven Program Synthesis" by Nadia Polikarpova
Strange Loop Conference
“for a motivating talk and explanation on what program synthesis is try this one”
2 HN recommenders · 2018–2024
talk#3145"A Little Taste of Dependent Types" by David Christiansen
Strange Loop Conference
“Here's an intro to dependent types from David Christiansen”
2 HN recommenders · 2018–2023
talk#3428Analyzing Programs with Z3
Compose Conference
“the best one I've found as an entry point was the approach they use in Cryptol”
2 HN recommenders · 2016–2021
explainer#3619How An Infinite Hotel Ran Out Of Room
Veritasium
1 HN recommenders · 2021–2022
talk#3762Robert Moss: Julia and the Next Generation Airborne Collision Avoidance System
The Julia Programming Language
“See these talks on how a collision avoidance system was designed with Julia.”
1 HN recommenders · 2016–2024
lecture#3779Five Stages of Accepting Constructive Mathematics - Andrej Bauer
Institute for Advanced Study
“Here are two versions of the same well-done talk, from Andrej Bauer”
1 HN recommenders · 2018–2026
talk#3785NVIDIA — Securing the Future of Safety and Security of Embedded Software (Captioned)
AdaCore
“The HN community may be interested in this 1 hour presentation [1] on Nvidia's adoption of Ada”
1 HN recommenders · 2022–2026
lecture#4261Scott Aaronson | How Much Math Is Knowable?
Harvard CMSA
“I learned about it in this Scott Aaronson talk,”
1 HN recommenders · 2025
talk#4278Type-Driven Development in Idris — Edwin Brady
Scala World
“Something like that is likely the future of programming!”
1 HN recommenders · 2019–2024
talk#4561seL4 Is Free – What Does This Mean For You?
Linux.conf.au 2015 -- Auckland, New Zealand
“The whole talk is well worth a watch.”
1 HN recommenders · 2015–2019
Channels HN cites most for logic & formal methods
Each channel page lists every video of theirs that HN recommends.
More in Mathematics & Theoretical CS