История изменений
Исправление hateyoufeel, (текущая версия) :
Какой бекенд? Компиляция? Agda давно компилируется и имеет прозрачный FFI с Haskell’ем
Ну вот ты им пользовался сам?
Lean с четвёртой версии (но она ещё допиливается, к сожалению) компилируется в C++, к полученным файлам можно потом произвольный C++ прикомпилировать, «@[extern]» там есть.
«Компилируется в C++» — это вообще ничего о скорости не говорит, сам понимаешь.
Исходная версия hateyoufeel, :
Какой бекенд? Компиляция? Agda давно компилируется и имеет прозрачный FFI с Haskell’ем
Ну вот ты им пользовался сам?
Lean с четвёртой версии (но она ещё допиливается, к сожалению) компилируется в C++, к полученным файлам можно потом произвольный C++ прикомпилировать, «@[extern]» там есть.
«Компилируется в C++» — это вообще ничего о скорости не говорится сам понимаешь.