Прочитал я тут, что Haskell и теория категорий уже не в моде среди диванных академиков, что будущее за Idris и зависимыми типами. С одной стороны, формальная верификация и доказательство корректности кода - это очень интересно. С другой, непонятно как использовать этот верифицированный код в реальном мире. Вот типичный пример из вики:
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a
total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil Nil = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys
Правильно ли я понимаю, что зависимые типы нужны только математикам для использования в доказателях теорем, и формально верифицированное ядро ОС или гарантированно корректный веб-сервер на Idris не написать?
P.S. В С++ есть функционально близкая фича в виде параметризированных значениями шаблонов, за 25 лет ей нашлось применение только в std::array, да еще для расчета факториалов при компиляции.
