foundations

José Valim's ElixirConf US 2023 closing keynote on the foundations of the Elixir type system, covering set-theoretic types and gradual typing with strong arrows.

Philip Wadler's Lambda Days talk on propositions as types, the link between logic and computation that underlies theorem provers and programming language design.

Psychologist Jonathan Haidt presents his moral foundations research in a TED talk. He argues that liberals and conservatives weigh a different set of moral values, which helps explain political divides.

Meredith Patterson and Sergey Bratus argue that networked software stays insecure because protocols and inputs are too complex to recognize safely. They propose using formal language theory and grammars to build secure, verifiable input handling.

Philip Wadler's Strange Loop talk on Propositions as Types, the link between logic and computation (the Curry-Howard correspondence). He traces its history through Church, Godel and Turing and shows how it shaped theorem provers and programming languages.

Mathematician Kevin Buzzard explains why he believes the Lean theorem prover will shape the future of mathematics, and describes digitizing his university curriculum in Lean with undergraduates, plus the cultural challenges.

Leslie Lamport argues that programmers, like architects, should write rigorous specifications before coding, especially for concurrent and distributed systems. The talk introduces the case for writing specs (the TLA+ mindset) as a way of thinking above the code.

Jay Parlar's Strange Loop talk shows how model checkers such as Alloy can find complex bugs in a system's design without running or reading any code. He walks through modeling architectures and checking every possible sequence of operations, including a real security bug and a UI feature-interaction bug.

Edwin Brady, creator of Idris, presents Idris 2 and demonstrates type-driven development, where the compiler assists by filling holes and suggesting implementations from types.

Guy Steele's PPoPP 2017 keynote surveying the history of computer science metanotation, including BNF, inference rules, and overline notation. He argues the field's notations are inconsistent and fragmented.

Edwin Brady presents Idris 2, a rewrite of the Idris dependently typed language, and shows type-driven development in practice. The demos show the compiler filling in whole functions from their types.

Aditya Siram introduces ATS, a statically typed ML-like language that compiles to C and offers type-safe pointer arithmetic and a full proof language. The Strange Loop talk shows off C interop, concurrency and verification features with non-trivial examples.

Hillel Wayne's PyCon 2018 talk on testing beyond pytest and mypy. It introduces property-based testing with the Hypothesis library and design-by-contract with dpcontracts, and shows how to combine them with an existing test suite.

Hillel Wayne's Strange Loop talk introducing TLA+ as a specification language for finding concurrency bugs in designs. It covers stalling, race conditions and dropped messages, with PlusCal examples.

A Clojure/conj 2016 talk demoing Barliman, a prototype smart editor that does program synthesis. Given a partial program and tests, it completes the program using a relational interpreter written in miniKanren.

Nadia Polikarpova's Strange Loop talk on program synthesis driven by refinement types, as in Synquid. It shows how rich type specifications can be turned into verified, executable code.

David Christiansen gives a Strange Loop 2018 introduction to dependent types, where one language serves for both compile-time and run-time code and programs unite with proofs. It draws on his book The Little Typer.

Tikhon Jelvis's Compose Conference talk on using the Z3 SMT solver to analyze and verify programs, including checking invariants with bounded loops. He demonstrates verifying programs in a small language by compiling them to Z3.

Robert Moss's JuliaCon 2015 talk describes using Julia as a specification language for ACAS X, the next-generation airborne collision avoidance system that succeeds TCAS.

An AdaCore webinar in which NVIDIA engineers explain why and how they adopted Ada and SPARK for security-critical firmware. It covers the business case and the engineering experience of the transition.

Edwin Brady, creator of Idris, introduces type-driven development in a dependently typed language. He shows types being written first and programs derived with interactive editing, then extends beyond simple examples to programs that interact with users and networks.

Gernot Heiser presents seL4, a microkernel with a mathematical proof connecting security properties to the binary code, and explains what its open-sourcing means for users. It covers its roles as a microkernel, separation kernel and hypervisor.

Sal Khan of Khan Academy argues that schools push students forward with gaps in their foundations, and that students should instead master concepts at their own pace. He compares it to building a house on an unfinished foundation.