Вы когда-нибудь задумывались, почему одни рассуждения убеждают, а другие рассыпаются при первой проверке? Дело не в красноречии — дело в логике, науке, которой более двух тысяч лет и которая до сих пор определяет, что считается правильным мышлением. Аристотель заложил её фундамент в Древней Греции, а его законы работают безотказно: от школьного спора до квантовых вычислений. Разбираемся, как устроена логика изнутри — без философии ради философии, а с конкретными правилами, схемами и ловушками, в которые попадают даже умные люди...

Почему среди программистов на Haskell бытует легенда, что если программа компилируется, то она верна? Почему мало смысла в споре между приверженцами статической и динамической типизации? Как превратить тип функции в теорему, а программу — в еë доказательство? Об этом и многом другом мы поговорим в мини-серии статей, посвящённой теории типов. Зачем? Когда речь заходит о типах и типизации в программировании, то в ход идут самые разные аналогии. Кто во что горазд! Типы сравнивают с наклейками на...