История изменений
Исправление q0tw4, (текущая версия) :
Ну я занимался верификацией на диплом (с недопаскаля в ACL2 конвертил и верифицировал там) и потом немного возился с dependent typами. Но всякие языки типа agda неудобны, idris жутко бажный, coq слишком старомоден. К Isabelle/HOL планировал приступить, но както мотивации не хватало. Жаль только времени потребуется, ну пару месяцев точно. Увлекающийся и специалист - разные люди.
Так что вопрос, есть ли еще надобность в сей специальности или всё, тут наняли, а больше подобного нету?
Исходная версия q0tw4, :
Ну я занимался верификацией на диплом (с недопаскаля в ACL2 конвертил и верефицировал там) и потом немного возился с dependent typами. Но всякие языки типа agda неудобны, idris жутко бажный, coq слишком старомоден. К Isabelle/HOL планировал приступить, но както мотивации не хватало. Жаль только времени потребуется, ну пару месяцев точно. Увлекающийся и специалист - разные люди.
Так что вопрос, есть ли еще надобность в сей специальности или всё, тут наняли, а больше подобного нету?