I discuss dependent types, which are types that can contain non-type programs. An example of a dependent type is a list whose type contains its length. Instead of just writing List<String> for a list that contains strings, dependent types include types like List<String, 5> that describe lists of exactly five strings. Dependent types can also be used to represent mathematics, in which case the programs that they describe count as proofs, and tools from programming can be used to write math.

Dependent types used to be something that really required a research background, but there has been a lot of progress on making them more user-friendly and on writing accessible introductions lately.

Languages mentioned:

• Idris is a self-hosted dependently typed language with type-level resource tracking
• Agda is a testbed for new ideas in dependently typed programming
• Lean 4 is a self-hosted dependently typed language that has a more conservative logical core than Idris or Agda, and attempts to appeal more to practicing mathematicians.
• Coq is a proof assistant based on dependent types that has been used to fully mathematically verify a C compiler

Books mentioned:

• The Little Typer, by Daniel P. Friedman and David Thrane Christiansen is an intro to the core ideas of dependent types, in dialog form
• Type Driven Development with Idris by Edwin Brady, the creator of Idris, describes an approach to programming that uses expressive types as a way to make programmers' lives easier
• Programming Language Foundations in Agda by Phil Wadler, Wen Kokke, and Jeremy Siek describes the use of Agda for both programming and proving
• Software Foundations is a series of books that use Coq as an introduction to mathematically rigorous software development in a proof assistant. It's how I initially learned these topics!