Pewnie gdzieś słyszałeś “Izomorfizm Curry’ego-Howarda” albo obiło Ci się o uszy “Propositions as Types”. A może nawet czytałeś coś o tym, ale szybko zrezygnowałeś, bo poziom abstrakcji wydał Ci się zabójczy. Tymczasem to pewien podstawowy fakt leżący głęboko u podstaw informatyki. W moim wystąpieniu postaram się Ciebie przekonać, że jest to nie tylko coś co jako programista intuicyjnie rozumiesz, używasz na co dzień w językach programowania, ale też, że pozwala on na tworzenie lepszych programów poprzez użycie wyrafinowanych typów do dowodzenia poprawności.