Idris 2 - Quantitative Types in Action

Explore the latest developments in Idris 2, a functional programming language with first-class types, in this 58-minute conference talk by Edwin Brady. Dive into the new core language based on Quantitative Type Theory (QTT) and discover how it supports linear types, allowing programmers to specify not only what a program can do but also when it's allowed to do it. Learn how the quantities in the type system provide enhanced expressivity and see practical demonstrations of implementing state machines and communicating systems with verified properties. Gain insights into interactive type-driven development and understand how programming becomes a conversation with the machine in Idris 2.