Исправление balsoft, (текущая версия) :
Идрис здесь был приведен как пример языка с зависимыми типами, который на практике позволяет проверять выход за границы динамически размерного вектора на этапе компиляции. Можете дальше пытаться мне доказать, что Идрис плохо, а Rust/C/etc – хорошо, но больше читать это сил моих нет.
Исходная версия balsoft, :
Идрис здесь был привден как пример языка с зависимыми типами, который на практике позволяет проверять выход за границы динамически размерного вектора на этапе компиляции. Можете дальше пытаться мне доказать, что Идрис плохо, а Rust/C/etc – хорошо, но больше читать это сил моих нет.