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

Я не знаю, как обстоят дела в образовании сейчас, но 10-15 лет назад ни в школе, ни в университете никто всерьёз не объяснял, что программирование имеет свои типы, каждый из которых требует особого типа мышления. Не то чтобы это покалечило чьи-то судьбы, но изучение программных дисциплин могло бы проходить гораздо быстрее, если на стадии закладки фундамента мы представили многообразие языков и подходов, а не зомбически учили C++ в его консольных проявления. Многие, сталкиваясь с необходимостью...