{"guid":"886ea506-9b1a-5bc4-a885-1002035c6c8f","title":"Intro to Lean 4: A language at the intersection of programming and mathematics","subtitle":null,"slug":"gpn22-483-intro-to-lean-4-a-language-at-the-intersection-of-programming-and-mathematics","link":"https://cfp.gulas.ch/gpn22/talk/WWMGVN/","description":"Type theory is the secret sauce that makes a programming language awesome. The more knowledge we can make the compiler aware of, the more we can rely on the compiler.\n\nBut what is the limit? What if we could take _make bad state unrepresentable_ to the mathematical extreme? What is a proof anyway, can you eat it? Come on a wonderful journey into the land of dependent types, where we try building type-safe SQL queries, and sweeten the deal with our own syntactic sugar.\n\nI give a compressed intro and overview of Lean 4, a purely functional, dependently typed programming language and interactive theorem prover. Knowledge of purely functional languages is *not* required.\n1. We start from zero. Introduction to Lean 4 syntax, side-by-side with Rust. Sum and product types, `List`, some easy intro examples.\n2. _Dependent types_: Example of `Vec`, i.e. lists with statically known length. Dependent pattern matching.\n3. _Propositions-as-types_: You can have logical `And` and `Or` in Rust, too! But how do you model forall quantifiers? How do you model `x \u003c= y` in the type system?\n4. Playing around with _types as first-class objects_, using heterogenous lists and projections on them as example.  You can't pattern match on types themselves, or... can you?\n5. _Metaprogramming_: Custom syntax, custom elaborators. Using what we learned to make type-safe SQL queries work, such as (note the absence of string quotes):\n```\nlet dragons : Table Dragon := [...here be dragons...]\nlet dragons2 : Table ?huh? := SELECT name, coins FROM dragons\n```\nCode samples from slides: https://gist.github.com/Kiiyya/5566f09b2d1af6aa0d85ba01179dcfdb","original_language":"eng","persons":["Kiiya"],"tags":["gpn22","483","2024","Science"],"view_count":727,"promoted":false,"date":"2024-05-31T14:30:00.000+02:00","release_date":"2024-05-31T00:00:00.000+02:00","updated_at":"2026-04-05T23:45:04.252+02:00","length":3638,"duration":3638,"thumb_url":"https://static.media.ccc.de/media/events/gpn/gpn22/483-886ea506-9b1a-5bc4-a885-1002035c6c8f.jpg","poster_url":"https://static.media.ccc.de/media/events/gpn/gpn22/483-886ea506-9b1a-5bc4-a885-1002035c6c8f_preview.jpg","timeline_url":"https://static.media.ccc.de/media/events/gpn/gpn22/483-886ea506-9b1a-5bc4-a885-1002035c6c8f.timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/events/gpn/gpn22/483-886ea506-9b1a-5bc4-a885-1002035c6c8f.thumbnails.vtt","frontend_link":"https://media.ccc.de/v/gpn22-483-intro-to-lean-4-a-language-at-the-intersection-of-programming-and-mathematics","url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_title":"Gulaschprogrammiernacht 22","conference_url":"https://api.media.ccc.de/public/conferences/gpn22","related":[],"recordings":[{"size":507,"length":3638,"mime_type":"video/webm","language":"eng","filename":"gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_webm-hd.webm","state":"new","folder":"webm-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2024-06-01T17:45:53.325+02:00","recording_url":"https://cdn.media.ccc.de/events/gpn/gpn22/webm-hd/gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/77585","event_url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_url":"https://api.media.ccc.de/public/conferences/gpn22"},{"size":202,"length":3638,"mime_type":"video/webm","language":"eng","filename":"gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_webm-sd.webm","state":"new","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2024-06-01T07:32:01.977+02:00","recording_url":"https://cdn.media.ccc.de/events/gpn/gpn22/webm-sd/gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/77482","event_url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_url":"https://api.media.ccc.de/public/conferences/gpn22"},{"size":152,"length":3638,"mime_type":"video/mp4","language":"eng","filename":"gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_sd.mp4","state":"new","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2024-05-31T19:34:21.143+02:00","recording_url":"https://cdn.media.ccc.de/events/gpn/gpn22/h264-sd/gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_sd.mp4","url":"https://api.media.ccc.de/public/recordings/77394","event_url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_url":"https://api.media.ccc.de/public/conferences/gpn22"},{"size":38,"length":3638,"mime_type":"audio/opus","language":"eng","filename":"gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_opus.opus","state":"new","folder":"opus","high_quality":false,"width":0,"height":0,"updated_at":"2024-05-31T19:24:25.043+02:00","recording_url":"https://cdn.media.ccc.de/events/gpn/gpn22/opus/gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_opus.opus","url":"https://api.media.ccc.de/public/recordings/77390","event_url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_url":"https://api.media.ccc.de/public/conferences/gpn22"},{"size":55,"length":3638,"mime_type":"audio/mpeg","language":"eng","filename":"gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_mp3.mp3","state":"new","folder":"mp3","high_quality":false,"width":0,"height":0,"updated_at":"2024-05-31T19:17:25.768+02:00","recording_url":"https://cdn.media.ccc.de/events/gpn/gpn22/mp3/gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_mp3.mp3","url":"https://api.media.ccc.de/public/recordings/77380","event_url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_url":"https://api.media.ccc.de/public/conferences/gpn22"},{"size":526,"length":3638,"mime_type":"video/mp4","language":"eng","filename":"gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_hd.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2024-05-31T18:59:16.585+02:00","recording_url":"https://cdn.media.ccc.de/events/gpn/gpn22/h264-hd/gpn22-483-eng-Intro_to_Lean_4_A_language_at_the_intersection_of_programming_and_mathematics_hd.mp4","url":"https://api.media.ccc.de/public/recordings/77367","event_url":"https://api.media.ccc.de/public/events/886ea506-9b1a-5bc4-a885-1002035c6c8f","conference_url":"https://api.media.ccc.de/public/conferences/gpn22"}]}