Да что вы говорите! И когда же зарождалось направление ФП?.. Какие же надежды были с ним связаны? ;)

ФП как направление, насколько я понимаю, зародилось в 60е и более-менее сформировалось в 70е годы прошлого века. С тех пор многие считали (и продолжают считать :)) что ФП - более совершенное и перспективное направление развития языков программирования, и с развитием вычислительных мощностей именно ФП-языки станут новым стандартом. Практика показала, что до сих пор этого не произошло.

Далее, про верификацию. Современные методы ПОЗВОЛЯЮТ перебрать все возможные варианты входных состояний и оценить, верные ли результаты при этом получаются - в 90е годы данное направление очень бурно развивалось, и достигнутые результаты по преодолению проблемы комбинаторного взрыва там впечатляют. Там по-прежнему масса нерешенных проблем - от большой вычислительной сложности (из-за которой трудно просчитать большие схемы) до ограничений на модели. По этой причине "серебряной пулей" эти методы не являются, и вполне естественно, что не существует софта, который бы на вход получал схему, а на выходе однозначно говорил, работает она или нет. Однако это не мешает серьезным производителям заниматься верификацией своей логики формальными методами, создавая для этого специализированные решения и модели.

В отношении "проверки идей" - обычно под термином "верификация" понимают все-таки не проверку идей, а проверку того, что определенная модель работает "правильно" - соответствует набору требований, полностью описывающих то, чего мы от этой модели хотим.

Да что вы говорите! И когда же зарождалось направление ФП?.. Какие же надежды были с ним связаны? ;)

ФП как направление, насколько я понимаю, зародилось в 60е и более-менее сформировалось в 70е годы прошлого века. С тех пор многие считали (и продолжают считать :)) что ФП - более совершенное и перспективное направление развития языков программирования, и с развитием вычислительных мощностей именно ФП-языки станут новым стандартом. Практика показала, что до сих пор этого не произошло.
Лямбда-исчисление - основа ФП, - было представлено логиком Алонсо Черчем (Alonso Church) в 1935 году. Машина Тьюринга была представлена Аланом Тьюрингом в 1936 году.

ЛИ разрабатывалась в качестве лишенного парадоксов (парадокс забыл, чего имени, Гильберта, по-моему) средства выражения вычислений. Не оправдало.

Это стандартная ловушка, в которую попадают все, кто думает, что знает историю.

Чисто функциональных языков раз-два и обчелся. Назову два самых известных, это Clean и Haskell. Они отличаются от ML/Lithp чистотой, там есть ядро, которое не позволяет побочных эффектов (referentially transparent core language). Haskell, так вообще - лямбда-исчисление с толстым слоем синтаксического сахара сверху.

Оный Хаскель появился в 1989 году, а первые реализации с нормальным вводом-выводом в 1992 году или позже. Это далеко не 70-е.

До этого главным событием были ML - вывод типов, сравнение с образцом, все очень удобно, - и Id90, язык с lenient порядком вычислений. Это секретное оружие dataflow, он эффективно распараллеливался до 64-х процессоров на Connection Machine 5, CM-5 (конец 80-х). Не пошел потому, что был "не Фортран" и из-за неудобства программирования (M-память может дать прикурить любому;).

Кстати, энергичный порядок вычислений (ML, LISP) не параллелится. Параллелится ленивый или lenient (ленивый - приводом к lenient, надо отметить). Собственно, Clean когда-то был Concurrent Clean, возлагались на него надежды, но он перестал им быть.

Современный Хаскель нормально параллелится, хоть и вручную, но очень просто. Он чист, эффективен и удобен в использовании.

Мне неизвестно про 70-е и 80-е в истории функциональных языков. Вся история творилась до конца 30-х и после 90-го, в промежутке была подготовка к рывку (Hindley-Milner type inference algorithm, inductive data types and pattern matching, G-machine и тп). Даже Id90 благополучно мигрировал в pH, а разработчики железа для него - в сторону multithreaded processors.

Теперь про моделирование.

Есть модели, на которых обкатываются архитектурные решения, как они себя поведут под настоящей нагрузкой, окупается ли большая площадь кристалла выгодой в скорости исполнения. Вот это случай как раз для Хаскеля, потому, что их надо сделать очень быстро.

И про проверку.

Synopsis, с их 800 PhD, решает проблему верификации очень просто - "мы генерируем случайные стартовые точки состояний и из них отправляем верификацию моделей; глубоко не ходим, ничего гарантировать не можем, объем очень большой; пользуйтесь тестами."

То, чем пользуется Интел, IBM и AMD внутри себя, на индустрию не влияет. Индустрия пользуется Synopsis, Cadence и прочими Mentor Graphics. И Synopsis, по-моему, лидер. ;)