Description

Elmの作者の新作Acadiaの記事を見ながらデータベースにアクセスするときのあれやこれやについて雑談しました。後半はLean言語や証明の価値についてのよもやま話です。

• tricot
• tricot - Wikipedia
• Rethinking Database Programming | Acadia
• Solving the 1+N Query Problem | Acadia
• ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 
• Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog 
• Lean Game Server (Natural Number Game) 

Chapters:
(00:00) Opening
(06:10) Rethinking Database Programming
(20:25) Solving the 1+N Query Problem
(27:12) Leanの勉強をしてみた
(37:25) 証明は結果が大事