Так что, может кто знает?😏

Там и с массивами не сказать, что тема раскрыта. В Клине, кмк, нужно продумывать библиотечные функции для работы с изменяемыми данными.

Они, кстати, в этом году обещались выпустить очередную версию.

Так есть ли чистый ФП ЯП, у которого нет проблем с оптимизацией? Минимум мутации, наличие конкуренции и желательно отсутствие GC.

Могу я предложить вам язык flow9? Изначально он задумывался как раз как практичный ФП язык. Мутабельность там есть, но это up to developer насколько использовать - можно вообще все чистым делать. Ну для себя я завел rule of thumb что 99% кода должны быть чистыми, в особом 1% допускается мутабельность. Параллельность - есть, асихронность - есть. Вообще, если хочется чего то такого-сякого, можно определить native типы и функции, которые в рантайме будут что то особое делать. Я, например, добавил в стандартую библиотеку вектора и хэш-таблицы (для особых случаев) как нейтивы. Но чтобы использовать такие нейтивы надо конечно их реализовать в рантайме. Язык кроссплатформенный и несколькими бэкэндами, ну то есть транслируется в собственный байткод, можно в джаву, с++, JS, есть ещё несколько бэкэндов, но они недоделанные. Можно наконец свой бэкэенд запилить.

Я делал extension для flow в vscode, так что кодить можно с удобством. Есть compile-сервер, который держит в оперативке сорцы и в результате компилится очень быстро, язык инкрементальный, т.е. скомпилированные модули кешируются и опять таки грузятся быстро. Вобщем мое лично мнение - ФП язык с человеческим лицом очень удобный для практики. И кстати можно писать достаточно эффективный софт на нем. Я лично для своей формальной математики использую (да и не только) - и доволен как слон.

Lean 4. 😄

Спасибо, посмотрю

Ну или Koka можно посмотреть.

Futhark? Хотя он не совсем general purpose

Вообще сам я думал переводить Coq-код в С и оптимизировать там, дополнительно добавив доказательство, что, эм, на "логическом" уровне программы эквивалентны, код на "физическом" уровне формально корректен, а затем компилировать в CompCert. Затем сравнить с тем, что компилируется сразу из Coq при помощи CertiCoq и далее CompCert. И затем сравнить производительность.

Но это много ручной работы.

Было бы можно писать внутри Coq / Gallina на C, было бы проще (сравнивать)

гц же

Если использовать CertiCoq, то мы получим Clight код, но он будет, эм, немного не таким, чтобы можно было проследить функциональное соответствие кода в нём и галлине в человекочитаемом смысле (не знаю, как сказать лучше). Без этого не получится различить "логический" и "физический" уровни С-программы, где в разрезе первого программа должна быть проверена (в смысле доказательства) на эквивалентность программы в галлине (всей), а в разрезе второго должна иметь доказательство корректности (быть верифицированной).

Вот и можно было бы сравнить ручные оптимизации кода в галлине при помощи C и то, что было бы получено автоматом при помощи CertiCoq

Не совсем. Там хитрая схема подсчёта ссылок, которая по большей части их как раз не считает. И immutable-but-in-place сверху.
В Koka тоже внедрили -- там уже и замеры с бенчмарками сделали.

А делали ли бенчмарки пруф-ассистентов?

Это ж смотря по каким критериям. 😉
Что-то когда-то видел, но какое-то наколеночное...

эх, хочется уже скорее прувер в свою систему ввернуть.... Но пока занят семантическим программированием - экспериментальный язык semprog: https://github.com/dmitry-vlasov/semprog.

10-го мая дедлайн в конференции frocos - я туда хочу кинуть материальчик по semprog'у, после этого уже наконец можно будет прувер запиливать.