История изменений
Исправление AndreyKl, (текущая версия) :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.
Что до Кока - писателей-практиков на нём лично я не встречал. Знакомые люди пишут, но всё хобби на сколько я знаю. Основное занятие для них - доказательства.
Если не лично - есть экстрактор из кока в окамль. Вроде есть даже верифицированный экстрактор в окамл. Наверное же пользуются.
Но всё таки мейнстрим вроде как для Кока - это доказательства.
Исправление AndreyKl, :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.
Что до Кока - писателей на нём лично я не встречал, кроме вот этого https://github.com/emarzion/coqtbgen . Но это вроде как хобби для него (если ничего не поменялось у него). И вот писатель на Коке (у него там несколько проектиков) https://github.com/clarus/coq-moment , но тоже по моему хобби. Основное занятие - доказательства, (если опять же ничего изменилось у него).
Если не лично - есть экстрактор из кока в окамль. Вроде есть даже верифицированный экстрактор в окамл. Наверное же пользуются.
Но всё таки мейнстрим вроде как для Кока - это доказательства.
Исправление AndreyKl, :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.
Что до Кока - писателей на нём лично я не встречал, кроме вот этого https://github.com/emarzion/coqtbgen . Но это вроде как хобби для него (не знаю точно). Но не лично - есть экстрактор в окамль. вроде есть верифицированный экстрактор в окамл. Наверное же пользуются.
Но всё таки мейнстрим вроде как для Кока - это доказательства.
ЗЫ. Ах, ну и вот писатель на Коке (у него там несколько проектиков) https://github.com/clarus/coq-moment , но тоже по моему хобби. Основное занятие - доказательства, (если ничего изменилось у него).
Исправление AndreyKl, :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.
Что до Кока - писателей на нём лично я не встречал, кроме вот этого https://github.com/emarzion/coqtbgen . Но это вроде как хобби для него (не знаю точно). Но не лично - есть экстрактор в окамль. вроде есть верифицированный экстрактор в окамл. Наверное же пользуются.
Но всё таки мейнстрим вроде как для Кока - это доказательства.
ЗЫ. Ах, ну и вот писатель на Коке (у него там несколько проектиков) https://github.com/clarus/coq-moment , но тоже по моему хобби. Доказательства - вот основное занятие.
Исправление AndreyKl, :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.
Что до Кока - писателей на нём лично я не встречал, кроме вот этого https://github.com/emarzion/coqtbgen . Но это вроде как хобби для него (не знаю точно). Но не лично - есть экстрактор в окамль. вроде есть верифицированный экстрактор в окамл. Наверное же пользуются.
Но всё таки мейнстрим вроде как для Кока - это доказательства.
Исправление AndreyKl, :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.
Что до Кока - писателей на нём лично я не встречал, кроме вот этого https://github.com/emarzion/coqtbgen . Но это вроде как хобби для него (не знаю точно). Но не лично - есть экстрактор в окамль. вроде есть верифицированный экстрактор в окамл. Наверное же пользуются.
Исходная версия AndreyKl, :
ха, повеселил. Но если ты про Кок и доказательства всякие, то там в первую очередь надо быть любителем теории типов (хотя любители теории категорий безусловно найдут своё место под солнышком). Ну про практику.. не знаю, пишут на Хаскелле, живут как-то . Даже тут на форуме несколько практиков есть.