Mathematica?

Да там есть, но это еще не делает ЯП чисто функциональным, лямбды много где есть. Хотя я с Mathematica мало знаком

Ну почти все элементы современного Функ прог

Mathematica это система переписывания термов с динамической типизацией.

Да, а Хаскель - со статической.

Только вот классическая система переписывания, в духе алгорифмов Маркова, вообще в лямбда-исчислении не нуждается. А как можно без лямбды? У всех ФП-шников стикеры с лямбдой, и в никах она преобладает... :)

Тогда у вас и R не фуекциональный- там нет символа лямбда

Только Питон и Хаскель

Я еще вижу кардинальное отличие в самом подходе к программированию. Интерактивное, исследовательское программирование это не совсем про современное ФП. А именно такой подход у той же Математики.

Короче, есть Хаскель и императивщина?

""Haskell is, in my view, the world’s best imperative programming language..." :)

а ещё эксель ))

Есть масса различных декларативных вариантов языков (потоковые (да, тот же Excel), логические, синхронные, комбинаторные...). Как итог — предлагаю все скопом не относить к ФП.

Короче ФП == Data.Void.Void?

Толково!

Ну вот кстати SMT ближе к constraint logic programming

Видимо только Excel и выживет.

Да, но может даже больше. Кстати, я недавно выяснил, что в последних версиях Z3 даже Datalog встроенный появился! :)

Там кое-что по круче даже, алгоритм называется PDR

А datalog как я понимаю сейчас уже только как baseline там для других алгоритмов

Скорее, видимо, как DSL. А за Даталогом могут стоять разные решатели.
Вообще, я думаю, что в какой-то момент в Z3 перейдут на нотацию общего программирования в ограничениях. Вот, кстати, где раздолье для компиляторщиков!
Есть, допустим CP-программа. Ее нужно проанализировать (и преобразовать) на предмет того, какой решатель в конечном итоге выбрать: SAT, MILP, fixed point и так далее. Очень интересная и актуальная задача.