Programowanie dowodami
Prowadzący: Radosław Rowicki
Nauczymy się masakrować bugi przy użyciu faktów i logiki
Opis
Nie powinno być niespodzianką, że wiele konceptów z informatyki i logiki jest powiązanych ze sobą tak silnie, że można wręcz je ze sobą scalić i traktować jak identyczne. Jednym z ciekawszych przykładów tego zjawiska jest tzw "izomorfizm Curry'ego i Howarda", który wskazuje na równoważność zdań logicznych oraz typów (takich jak znany i lubiany int). Ekwiwalentnie, dowody owych twierdzeń zrównywane są z wartościami reprezentującymi te typy. W ten sposób można by rzec że 3 jest "dowodem" na inta.
Na warsztatach wprowadzę was w podstawy programowania funkcyjnego w jęzku o majestatycznej nazwie Coq /kok/. Język ten, jak nazwa absolutnie nie wskazuje, jest znany przede wszystkim jako narzędzie do pół-automatycznego dowodzenia twierdzeń matematycznych oraz weryfikacji własności programów. Wspomniany wcześniej izomorfizm jest tym co sprawia, że to pozornie dziwne zastosowanie ma sens, a to wszystko dzięki POTĘŻNEMU systemowi typów jaki oferuje Coq.
Plan
- Poznamy Coq jako funkcyjny język programowania. Nauczymy się pisać proste programy funkcyjne i operować funkcjami wyższych rzędów.
- Zagłębimy nieco w teoretyczne podstawy teorii typów i zastanowimy się co tam się dzieje pod spodem.
- Znienacka wjedzie logika. Ale nie taka zwykła logika co ty gadasz mówie ci złą logikę miałeś ja ci załatwie inną spróbuj ja ci co jakie w liceum była co ty gadasz inną musisz spróbować bo różne sa
- Napiszemy nasze pierwsze twierdzenie w Coq i udowodnimy je tylko po to by ogarnąć że już to zrobiliśmy wcześniej
- Poznamy język taktyk dowodowych oferowanych przez Coq żeby sprawniej trzaskać dowodziki
- W zależności od czasu, będziemy tłuc dowody na liczbach naturalnych, listach, może nawet drzewach i będziemy masakrować bugi przy użyciu faktów i logiki
Wymagania
Wymagane cechy i umiejętności:
- Rozumienie indukcji matematycznej
- Ogarnianie rekurencji
- Programowanie w jakimś języku, najlepiej ze statycznymi typami (dla pythoniarzy mypy)
- Komputer i umiejętność instalowania rzeczy na nim
Przydatne rzeczy
- Jeśli Python to jedyny język jaki znasz, polecam zapoznać się z https://mypy-lang.org/
- Biblia izomorfizmu Curry'ego i Howarda (oraz rachunku lambda): https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Przyjemny kalkulator lambd i wstęp do rachunku: https://crypto.stanford.edu/~blynn/lambda/ (może trochę spoilerować zadanka)
- Jeśli planujesz przyjść z niemowlakiem, ta gra powinna dobrze przygotować go do zajęć: https://worrydream.com/AlligatorEggs/
Kontakt
Można pisać na maila radrowicki w popularnej domenie Googla.