Без заголовка

А в чем маргинальность к примеру Coq или HOL? Это серьезные инструменты, которыми применимы для промышленных проектов. Юзербейз у них достаточно большой. У Coq первый релиз был 30 лет назад. Просто это требует очень высокой квалификации, чтобы задействовать эти тулзы в промышленном проекте (не токо инженеров, а ваще). У меня есть подозрение что маргинальность немного в другом проявляется - в том смысле, что в некоторых странах просто исчезающе мало места для проектов, где их можно было бы применить. Но если с мировой точки зрения смотреть, то маргинальны как раз такие страны, которые не могут осваивать современные технологии (а они заопенсорщены, даже Микрософт свой Z3 заопенсорсило). Adam Chlipala полагает что в течении 10 лет формальные тулзы созреют настолько, что от них будет польза для гораздо более широкого набора проектов. https://media.ccc.de/v/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development Я лично с ним согласен, хотя может и чутка подольше :). Но не суть важно. Важно, что это уже real thing пусть пока еще дорогой и не всем доступный. Но я вот рассчитываю в следующем году применить для реального проекта формальные тулзятины. Лет десять пытался но не вышло, сейчас вот очередная итерация надеюсь будет.