LINUX.ORG.RU

Coq 8.5

 ,


3

7

Тихо и незаметно вышла новая версия системы интерактивного доказательства теорем Coq (Петух).

Система Coq предоставляет язык Gallina (Курица) — функциональный язык с зависимыми типами, основанный на исчислении индуктивных конструкций. Особенностью данной системы является наличие особого подъязыка тактик доказательства (в отличии от, например, Агды, в которой пользователь конструирует элемент типа, являющийся доказательством, в явном виде с использованием интерактивного интерфейса, основанного на Emacs).

Coq используется как собственно в математике, так и для так называемого сертифицированного программирования — написания программ вместе с доказательством их корректности.

Основные новшества в версии 8.5:

  • асинхронное редактирование документов в CoqIDE, позволяющее работать с текущим доказательством, в то время как Coq проверяет другие доказательства в фоне;
  • полиморфизм относительно универсумов, позволяющий использовать одни и те же определения для универсумов разного уровня;
  • примитивные проекции, улучшающие временную и пространственную эффективность для записей и добавляющие для них эта-конверсию;
  • новый движок тактик;
  • новая процедура редукции native_compute, позволяющая вычислять термы, используя нативный компилятор OCaml'а;
  • новый быстрый режим компиляции, пропускающий проверку доказательств;
  • новая опция -type-in-type, позволяющая объединять иерархию типов в один универсум (делает логику несогласованной, но упрощает эксперименты);
  • заметное улучшение эффективности в целом.

>>> Новость

anonymous

Проверено: maxcom ()
Последнее исправление: Wizard_ (всего исправлений: 2)

имхо, действительно стало работать немного быстрее.

ymn ★★★★★
()

Не по теме, но...

По английски «петух» — это cock. Почему coq перевели, как «петух».

anonymous
()
Ответ на: комментарий от A1

В мире есть программисты говорящие на других языках, внезапно

А теперь, внезапно поясни свою мысль. В каком-таком языке «coq» — это петух.

anonymous
()
Ответ на: комментарий от theNamelessOne

Внезапно, во французском.

Внезапно удивлён. Пасиба тебе внезапно, незнал.

anonymous
()
Ответ на: комментарий от theNamelessOne

Есть польза рядовому быдлокодеру от изучения и использования сабжа?

Если ты быдло, то тебе тут нечего делать. Язык для илиты.

anonymous
()

Есть у сабжа история успеха, а то я тут на их ключевые слова посмотрел: if, IF, exists, exists2. Стали терзать меня смутные сомнения.

A-234 ★★★★★
()
Ответ на: комментарий от d_a

выше уже слоубро кинули же статью из вики про вид джавагоспод

anonymous
()

Coq используется ... для ... написания программ вместе с доказательством их корректности

И где эти программы потом используются? (вопрос не про отрасли народного хозяйства, а про конкретные устройства)

Кто-нибудь тут занимается написанием таких программ фулл-тайм? Если да, то у какого работодателя?

Manhunt ★★★★★
()
Ответ на: комментарий от A-234

Довольно широко применяется в академических исследованиях.

Иногда результаты этих исследований вполне себе юзабельны — http://compcert.inria.fr/

ymn ★★★★★
()
Ответ на: комментарий от ymn

Coq используется как собственно в математике, так и для так называемого сертифицированного программирования — написания программ вместе с доказательством их корректности.

Программы пишутся на языке программирования. Я и спрашиваю, на каких языках программирования можно писать доказанно корректные программы? Или на этом самом Coq их и надо писать?

Legioner ★★★★★
()
Ответ на: комментарий от Legioner

Или на этом самом Coq их и надо писать?

Да. С последующим преобразованием искаропки в хаскель, окамл или схему.

ymn ★★★★★
()
Ответ на: комментарий от ymn

Понятно, спасибо. Остаётся вопрос корректности преобразователей и компиляторов, пока это всё дойдёт до машинного кода, но в целом понятно.

Legioner ★★★★★
()

системы интерактивного доказательства теорем
Coq (Петух)

А линуксоеды с ее помощью смогут доказать вендекапец?

anonymous
()

Тихо и незаметно вышла новая версия системы интерактивного доказательства теорем Coq (Петух).

Система Coq предоставляет язык Gallina (Курица)

следующая итерация видимо будет Egg (Яйцо), для выяснения вопроса его первичности с курицей :-)

MKuznetsov ★★★★★
()
Ответ на: комментарий от anonymous

Галина - это по испански же. Кубики галина бланка же.

Gallus (латынь) — петух. Gallina — курица в большинстве языков романской группы.

По теме: как Coq'ом доказать теорему «о первичности яйца или курицы»? :)

quickquest ★★★★★
()
Ответ на: комментарий от anonymous

Языку Gallina нужна билблиотека Natasha (Овца).

Froggies are sick bastards.

anonymous
()
Ответ на: комментарий от anonymous

Галина - это по испански же. Кубики галина бланка же.

Испанский и французский - это как русский и хохлятский же.

anonymous
()

Здравствуйте!

Не погибает ничто - поверьте ! - в великой вселенной. Овидий.

anonymous
()
Ответ на: комментарий от theNamelessOne

О! непосредственная! Есть шанс превратиться в небыдло! :)

gns ★★★★★
()
Ответ на: комментарий от upcFrost

Двойное «ll» читается как «й».

Зависит от диалекта. В нормативном кастильском «й» и «льль» — разные звуки. В Америках — один и тот же «й».

anonymous
()

Gallina (Курица)

ЛОР познавательный: вот так я понял что пресловутая Галина Бланка - это белая курица!

robert_foster ★★
()
Ответ на: Не по теме, но... от anonymous

Внезапно, по английски петух будет cock.- характерно англ языку Ирландии/Великобритании, а также rooster - всего остального англоязычного мира (Североамериканского и австралийского «диалектов»).
См. также: рус «Петух» === укр «Півень» === укр. «Когут»

FeyFre ★★★★
()
Ответ на: комментарий от kto_tama

оно умеет доказывать теоремы ?

нет. оно умеет помогать их доказывать и проверять результат

сейчас, в общем-то, в академическом мире theorem prover по умолчанию - именно Coq; показательный пример - унивалентные основания Воеводского

jtootf ★★★★★
()
Ответ на: комментарий от Octagon

как доказать теорему
Неплохо бы начать с нормальной формулировки.

Теорема: {∀ курица ⊇ яйцо} :⇔ {∀ яйцо ↦ курица }

Докажи :)

quickquest ★★★★★
()

Coq is written in the Objective Caml language, with a bit of C. It is distributed under the GNU Lesser General Public Licence Version 2.1 (LGPL).

hobbit ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.