LINUX.ORG.RU

Programming Languages Software Award

 


0

1

В этом году приз Programming Languages Software Award достался Coq.

!Ъ: тыц

Ъ:

The Coq proof assistant provides a rich environment for interactive development of machine-checked formal reasoning. Coq is having a profound impact on research on programming languages and systems, making it possible to extend foundational approaches to unprecedented levels of scale and confidence, and transfer them to realistic programming languages and tools. It has been widely adopted as a research tool by the programming language research community, as evidenced by the many papers at SIGPLAN conferences whose results have been developed and/or verified in Coq. It has also rapidly become one of the leading tools of choice for teaching the foundations of programming languages, with courses offered by many leading universities and a growing number of books emerging to support them. Last but not least, these successes have helped to spark a wave of widespread interest in dependent type theory, the richly expressive core logic on which Coq is based.

As a software system, Coq has been in continuous development for over 20 years, a truly impressive feat of sustained, research-driven engineering. The Coq team continues to develop the system, bringing significant improvements in expressiveness and usability with each new release.

In short, Coq is playing an essential role in our transition to a new era of formal assurance in mathematics, semantics, and program verification.

★★★★★

Ответ на: комментарий от nokachi

это не вопрос, а информационное сообщение)

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

ymn ★★★★★ ()

Мне кажется, или на ЛОРе начинает уходить мода на Lisp, которую вытесняет мода на Coq и Agda?

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

Мне кажется, или на ЛОРе начинает уходить мода на Lisp, которую вытесняет мода на Coq и Agda?

Ну, это закономерный процесс. Одно время лисп и хаскелл были таким вот «матаном для посвящённых», сокровенным знанием. Потом началась популяризация: на густой аромат нонконформизма слетелись тысячи желающих быть «не-такими-как-все». Текущая ситуация такова, что на ЛОРе уже каждый школьник знает, что монада - это всего-навсего моноид в категории эндофункторов, а Рич Хикки ни черта не смыслит в гигиенических макросах.

Таким образом, лисп и хаскелл утратили элитарность. Поэтому появилась потребность в чём-то, что могло бы снова занять нишу. Этим и объясняется растущая популярность теорката и сопутствующих языков: Coq, Agda, Epigram, Omega и прочих.

anonymous ()

Если маргинальчеги сами себя не похвалит, то никто не похвалит.

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

анон эту пасту в каждое сообщение вставляет.

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

Таким образом, лисп и хаскелл утратили элитарность.

Это же просто отлично. Остались только вменяемые разработчики на этих языках, а тролли и небыдло разбежались на топик-подобные свистульки-блестяшки. Лисп и Хаскель можно поздравить с готовностью к интерпрайзам и другим подобным реал-ворлд-аппликейшинам.

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

Если не форсить, то количество и не вырастет.

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

Лисп и Хаскель можно поздравить с готовностью к интерпрайзам и другим подобным реал-ворлд-аппликейшинам.

Как бы давно уже используются... но, конечно, не в тех масштабах, как си, ява, си-шарп или питон. И слава Богу! У популярности всегда есть оборотная сторона.

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

Лисп и Хаскель можно поздравить с готовностью к интерпрайзам и другим подобным реал-ворлд-аппликейшинам.

Ну-ну, не прошло и пятидесяти лет.

anonymous ()

The award includes a prize of $2,500

маловато будет.

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

Например, идеи постройки летательных аппаратов тяжелее воздуха ждали своей реализации несколько веков. Ну и что?

И на чем ты сейчас предпочтешь слетать в другую страну? На самолете или воздушном шаре?

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

У популярности всегда есть оборотная сторона.

И не одна ;)

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

Ну, это закономерный процесс. Одно время лисп и хаскелл были таким вот «матаном для посвящённых», сокровенным знанием. Потом началась популяризация: на густой аромат нонконформизма слетелись тысячи желающих быть «не-такими-как-все». Текущая ситуация такова, что на ЛОРе уже каждый школьник знает, что монада - это всего-навсего моноид в категории эндофункторов, а Рич Хикки ни черта не смыслит в гигиенических макросах.

Таким образом, лисп и хаскелл утратили элитарность. Поэтому появилась потребность в чём-то, что могло бы снова занять нишу. Этим и объясняется растущая популярность теорката и сопутствующих языков: Coq, Agda, Epigram, Omega и прочих.

Ну вот взял и все раскрыл. ;)

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

Ну, это закономерный процесс. Одно время лисп и хаскелл были таким вот «матаном для посвящённых», сокровенным знанием. Потом началась популяризация: на густой аромат нонконформизма слетелись тысячи желающих быть «не-такими-как-все». Текущая ситуация такова, что на ЛОРе уже каждый школьник знает, что монада - это всего-навсего моноид в категории эндофункторов, а Рич Хикки ни черта не смыслит в гигиенических макросах.

Большинство обитателей лора и сейчас не знают, что такое монады, не разбираются в матане и даже не понимают чем макросы CommonLisp отличны от макросов Scheme. А желающие быть «не-такими-как-все» - скорее ухватываются за что-то более «красивое, модное, молодежное» а-ля Ruby, а не берут маргинальные языки и идеи. А такие как ты, прихлебатели мамкиного борща, любящие рассуждать о серебряных пулях и неактуальности оных, нонконформизме и его влиянии на неокрепшие умы таких как ты.

Таким образом, лисп и хаскелл утратили элитарность.

Не утратил, так как такого понятия у нормальных людей нет. Оно есть только в мозгу такого как ты, школьника не осилившего сложного инструмента, гнобимого фанбоями этого инструмента. Ну так вот, дорогой мой, пойми - те кто загнобил тебя, лишь такое же школоло и фанбои как и ты. По правде понимающих все нюансы идей и идеологии - единицы. А они даже не будут говорить с упырями, делящими людей на касты.

Поэтому появилась потребность в чём-то, что могло бы снова занять нишу.

Хочешь сказать фанбои лишпа и хацкеля вымерли? Лично каждого проверил?

Этим и объясняется растущая популярность теорката и сопутствующих языков: Coq, Agda, Epigram, Omega и прочих.

Если ты считаешь, что теоркат стал популярен из-за популяризации хацкеля и лишпа, то я тебе сочувствую. Это значит ты настолько ущербное и никчемное школоло, каких поискать еще надо. Советую для начала прочитать букварь или убраться куда положено - в биореактор, спасающий нацию.

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