Home › Topics › Mathematics & Theoretical CS
Logic & formal methods: videos Hacker News recommends
Logic and formal verification: proof assistants, Coq, Lean, TLA+, type theory and proofs, SAT solvers, model checking, program correctness, foundations of mathematics, set theory. Below: every video in this topic that at least three HN users linked with real commentary, in at least three different months (20 talks, 6 lectures, 5 explainers), best-scored first, with the comments on each video page.
- 9 HN recommenders 10 months 2012–2024HN repeatedly recommends it as the clearest and most correct beginner explanation of monads, with several commenters saying it finally made them click.
- 9 HN recommenders 9 months 2012–2024HN commenters call it one of the best security talks and the standard introduction to LANGSEC, which they use to argue for simpler, well-specified input formats.
- 9 HN recommenders 8 months 2015–2026HN regards it as an entertaining and eye-opening introduction to why logic and functional programming are connected, and it is a frequent pick in favorite-tech-talk threads.
- 7 HN recommenders 7 months 2021–2024HN commenters recommend it as a clear, accessible introduction to incompleteness and the self-referential proof idea.
- 6 HN recommenders 7 months 2015–2024Recommended as an accurate, entertaining on-ramp to set theory and infinity, worth pausing and rewatching.
- 9 HN recommenders 7 months 2019–2025Recommended as the clearest mathematician's perspective on formal proof assistants and why mathematics should be formalized.
- 5 HN recommenders 5 months 2015–2026HN points people to it as Lamport's own case for thinking and writing a spec before coding, and as an entry point to TLA+.
- 6 HN recommenders 5 months 2016–2022HN recommends it as the most accessible introduction to what lies beyond infinity.
- 4 HN recommenders 4 months 2019–2023HN commenters point to it as the best practical introduction to Alloy and to lightweight formal modeling.
- 4 HN recommenders 4 months 2019–2023Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.
- 3 HN recommenders 4 months 2014–2022HN people recommend it as a clear introduction to different sizes of infinity that non-mathematicians can follow.
- 3 HN recommenders 4 months 2018–2023G Guy Steele · talkHN recommends it as an excellent talk on notation problems, useful when reading papers or designing a new metalanguage.
- 5 HN recommenders 4 months 2018–2024HN points to it as a good introduction to Idris 2 and a striking demonstration of what dependent types enable.
- 4 HN recommenders 4 months 2017–2022Cited in Rust and systems-language threads as the best introduction to ATS, a language claimed to go beyond Rust's safety guarantees.
- 3 HN recommenders 3 months 2018–2023HN commenters point to it as a concise, convincing case for better testing practice short of full formal methods.
- 3 HN recommenders 3 months 2017–2018HN users recommend it as a good discrete math course for programmers, praising Leighton's relatable stories that motivate new concepts.
- 3 HN recommenders 3 months 2017–2019Recommended as a thought-provoking lecture from a Fields medalist on the foundations of mathematics and formal proof verification.
- 3 HN recommenders 3 months 2018–2025Recommended as a concise, high-level intro to what TLA+ is and when it helps.
- 3 HN recommenders 3 months 2017–2021Recommended as a companion to reading the dense book.
- 2 HN recommenders 2 months 2022–2024T The Power of Prolog · tutorialHN recommends it as the best short introduction to what makes Prolog unique.
- 2 HN recommenders 2 months 2016–2021Recommended as an exceptional whirlwind tour of the foundations of computer science.
- 3 HN recommenders 2 months 2017–2024HN people point to it as an amazing demonstration of relational programming and program synthesis that still looks exciting after LLM code generation.
- 2 HN recommenders 2 months 2018–2024HN points to it as a motivating introduction to what program synthesis is and what types can do for it.
- 2 HN recommenders 2 months 2018–2023Recommended as an approachable introduction to dependent types and a preview of what The Little Typer covers.
- 2 HN recommenders 2 months 2016–2021C Compose Conference · talkHN lists it among the practical entry points for learning Z3 and formal verification.
- 1 HN recommenders 1 months 2021–2022HN mentions it as a related, well-made Veritasium video when infinity and Hilbert's hotel come up.
- 1 HN recommenders 1 months 2016–2024HN points to it as a real-world example of Julia used in safety-critical aerospace design.
- 1 HN recommenders 1 months 2018–2026Pointed to as a well-done introduction to constructive mathematics when it comes up in logic and proof assistant threads.
- 1 HN recommenders 1 months 2022–2026A AdaCore · talkHN cites it in Rust-versus-C++ and Ada discussions as a real industrial case of choosing SPARK for safer embedded code.
- 1 HN recommenders 1 months 2025H Harvard CMSA · lecturePointed to in Busy Beaver threads as an accessible expert talk on the topic.
- 1 HN recommenders 1 months 2019–2024S Scala World · talkHN points to it as a demonstration of type-directed editing with typed holes, which some see as a likely future of programming.
- 1 HN recommenders 1 months 2015–2019L Linux.conf.au 2015 -- Auckland, New Zealand · talkCited to explain what formal verification of seL4 guarantees, such as ruling out whole classes of bugs like buffer overflows.
- cited 4× 0 months 2022–2023P Prolog Heritage · documentaryCited in Prolog threads as a rare documentary on the language's origins, with proper subtitles despite being in French.
Questions
What is the most recommended logic & formal methods video on Hacker News?
Brian Beckman: Don't fear the Monad by jasonofthel33t: HN repeatedly recommends it as the clearest and most correct beginner explanation of monads, with several commenters saying it finally made them click.
How is this logic & formal methods list ranked?
By HackerTube's score: the number of distinct months in which an HN comment recommended the video, plus half a point for every month with a strong recommendation. One viral thread counts less than steady recommendations over years.
Where do the videos come from?
From every Hacker News comment between 2007 and 2026 that linked a YouTube video, labeled by an AI model as a recommendation, a citation, a joke or a criticism. The list is published by HackerTube under ODC-By 1.0; this edition adds indexable pages and the comment context.
Video list and Hacker News comment labels from HackerTube (prompted by @karpathy), released under ODC-By 1.0, built on the open-index/hacker-news archive. Hacker News data is provided by Y Combinator; comments remain the work of their authors. Video titles, channel names and thumbnails belong to their creators and are shown via YouTube. HackerTube Watch is an unofficial edition. Data export of 2026-10-31.