Не, ну это холивар :-D
Agda лучше интегрируется с Haskell, чем Coq с OCaml.
Но плюс Coq'а действительно в учебниках и намного большей истории.
А предпочтения все же берут начало не со спора «Agda или Coq», а со спора «Haskell или OCaml», но это уже действительно холивар.
Я не пиарюсь, но вот статья на хабре. Может прояснится.
Честно говоря, вряд ли такие вещи будут использоваться повсеместно в реальных проектах, а тем более в Web.
Но вообще штука очень даже интересная.
Реальное для нее применение — автоматическая проверка доказательств — такое действительно часто встречается.
>… чтобы соблазнить упрямого программиста прочитать его. Что-нибудь типа «Что делать с плохим кодом»…
>… такой же птенец, как и все остальные…
Мне всегда было интересно, как можно легко подвести человека к самокритике. У меня никогда не получалось. Я использовал те же фразы по своей сути, но ваша форма изложения оказалась великолепной.
И конечно спасибо за статью — показана действительно интересная задача решаемая данным подходом.
Agda лучше интегрируется с Haskell, чем Coq с OCaml.
Но плюс Coq'а действительно в учебниках и намного большей истории.
А предпочтения все же берут начало не со спора «Agda или Coq», а со спора «Haskell или OCaml», но это уже действительно холивар.
Честно говоря, вряд ли такие вещи будут использоваться повсеместно в реальных проектах, а тем более в Web.
Но вообще штука очень даже интересная.
Реальное для нее применение — автоматическая проверка доказательств — такое действительно часто встречается.
… хотя я тогда бы это не увидел.
Я бы с удовольствием посмотрел, но либо свободное распространение, либо в топку.
Они что историю Smalltalk'a не знают?
Автор оригинального текста не пришел бы к вам на работу.
>… такой же птенец, как и все остальные…
Мне всегда было интересно, как можно легко подвести человека к самокритике. У меня никогда не получалось. Я использовал те же фразы по своей сути, но ваша форма изложения оказалась великолепной.
Браво!
А я все внимательно прочитал. Спасибо, очень захватывающе.
> и более чистом коде на «плюсах»
Чище чем на чем интересно?
Большое спасибо!