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

Дрейф начали вы и большое спасибо за предложение его прекратить. >Ибо все эти Haskell и OWL мне кажутся одинаково далёкими от удобства вычисления на человеческом хардвере, и одинаково неудобными способами выражения окружающего мира. В любом случае это будет конструктивная логика. Никуда от неё не деться. Является ли OWL реализацией конструктивной логики, мне неизвестно. Я даже не знаю, что это такое. Haskell является реализацией конструктивной логики. Agda2 ещё ближе (это реализация теории типов Пера Мартина-Лёфа). Поэтому практически любая попытка выразить что-то, компилируемое в железо, будет содержать в себе три четверти реализации Haskell и половину реализации Agda2.