Programowanie z dowodzeniem twierdzeń

Prowadzący: Piotr Masłowski

Jak napisać program i udowodnić komputerowi, że działa on dobrze
Zadania kwalifikacyjne
Kategorie: informatyka informatyka teoretyczna

λΠω

Opis

Typy. Niektórzy ich nienawidzą, inni je kochają. Pozwalają odrzucić nonsensowne programy (jak mnożenie napisów przez siebie), ale co jeszcze można dzięki nim osiągnąć?

Okazuje się, że wiele ciekawych i przydatnych rzeczy:

  • można napisać zip który bierze tylko listy tej samej długości
  • można całkowicie wyeliminować wyjątki (try-catch)
  • można wykazać, że 2 + 2 = 4
  • można zabronić dzielenia przez zero
  • można (czasami) zastąpić testy dowodami
  • można budować niezawodne maszyny stanów
  • można stworzyć typ Fin n – zawierający jedynie liczby 0, 1, … n-1

a wszystko to ze 100% gwarancją od kompilatora.

Tutaj zobaczymy jak wyglądają i działają w praktyce języki z zaawansowanymi systemami typów oraz poznamy trochę matematyki stojącej za nimi. Nauczymy się jak można z ich pomocą wyrażać twierdzenia (i ich dowody) o naszych strukturach danych, liczbach czy innych obiektach matematycznych. Poznamy również jak nie przejmować się programowaniem defensywnym, obsługą niemożliwych błędów, ani nawet czasem gdy nie jest on potrzebny. Przekonamy się też, że komputery są w stanie pisać za nas kod – również bez pomocy dużych modeli językowych

Plan

  1. Poznamy język Idris
  2. Zobaczymy w jaki sposób typy mogą odpowiadać twierdzeniom, a wartości – dowodom
    (izomorfizm Curry'ego-Howarda)
  3. Napiszemy kilka prostych dowodów z teorii liczb i z teorii grup
  4. Zobaczymy jak wygląda printf który nie jest w stanie nas zawieść
  5. Poznamy techniki pisania przyjemnego i eleganckiego kodu

Wymagania

  • Zrozumienie zadań kwalifikacyjnych
  • (albo) Znajomość rachunku lambda w różnych odmianach (z typami prostymi, System F, a najlepiej z typem Π)
  • (oraz) Komputer z zainstalowanym kompilatorem idris2 (w razie czego pomogę)

(powyższe (spójniki) nie podlegają normalnej kolejności działań)

Przydatne rzeczy

  1. look what they need, to mimic a fraction of our power /s
  2. jak się spojrzy kilka lat do tyłu, to rachunek lambda już się pojawiał
  3. jak ktoś chce od razu zanurkować w matematycznej teorii
  4. kalkulator lambd (i nie tylko)

Kontakt

W razie problemów czy wątpliwości śmiało piszcie na piotr@maslowski.xyz