Исправление AndreyKl, (текущая версия) :
Гм, спасибо за поясление.
Я попробую выразиться по-другому.
И с (условным) Идрисом/Коком/Агдой и без него у тебя есть проблема с отказом железа.
Но это отдельная проблема - проблема железа. Так же существует проблема взаимодействия с другими программами, которые могут работать неверно. И эта проблема тоже существует и в условном Питоне и в условном Идрисе.
Но _подавляющее_ большинство ошибок в программе - это ошибки программиста написавшего эту программу.
И вот тут есть существенная разница: Идрис позволяет гарантировать что этих ошибок просто нет. Понимаешь? Нет целых классов ошибок - неожиданного падения, неверных ответов, необработанного ввода... Более того, нет не потому что ты тесты не написал и они их не поймали и их вроде как «нет», а _гарантировано_ нет. (Ну, с точностью до ошибки в компиляторе идриса.. а то был как то пару лет назад случай, человек написал программу, верифицировал, всё, а она сегфолтится :) .. но это уже казусы невзрослого компилятора, конечно)
А по поводу раста в ядре - я думаю надо пробовать, очень интересно поглядеть на результат. По-моему весьма стоит.
Исходная версия AndreyKl, :
Гм, спасибо за поясление.
Я попробую выразиться по-другому.
И с (условным) Идрисом/Коком/Агдой и без него у тебя есть проблема с отказом железа.
Но это отдельная проблема - проблема железа. Так же существует проблема взаимодействия с другими программами, которые могут работать неверно. И эта проблема тоже существует и в условном Питоне и в условном Идрисе.
Но _подавляющее_ большинство ошибок в программе - это ошибки программиста написавшего эту программу.
И вот тут есть существенная разница: Идрис позволяет гарантировать что этих ошибок просто нет. Понимаешь? Нет целых классов ошибок - неожиданного падения, неверных ответов, необработанного ввода... Более того, нет не потому что ты тесты не написал и они их не поймали и их вроде как «нет», а _гарантировано_ нет. (Ну, с точностью до ошибки в компиляторе идриса.. а то был как то пару лет назад случай, человек написал программу, верифицировал, всё, а она сегфолтится :) .. но это уже казусы невзрослого компилятора, конечно)