Мне кажется String в BaconBox лишний.

И конечно спасибо за статью — показана действительно интересная задача решаемая данным подходом.

Не, ну это холивар :-D
Agda лучше интегрируется с Haskell, чем Coq с OCaml.
Но плюс Coq'а действительно в учебниках и намного большей истории.
А предпочтения все же берут начало не со спора «Agda или Coq», а со спора «Haskell или OCaml», но это уже действительно холивар.

Я не пиарюсь, но вот статья на хабре. Может прояснится.
Честно говоря, вряд ли такие вещи будут использоваться повсеместно в реальных проектах, а тем более в Web.
Но вообще штука очень даже интересная.
Реальное для нее применение — автоматическая проверка доказательств — такое действительно часто встречается.

Pascal! Браво! Так им!

Лучше, но об этом лучше не при людях.
… хотя я тогда бы это не увидел.

Перечитайте еще раз весь хабр :-D

Ни у кого!

Наверное лучшее введение в комбинаторную логику и лямбда исчисление для чайников :)

Упс, промазал :)

Оно что платное?
Я бы с удовольствием посмотрел, но либо свободное распространение, либо в топку.
Они что историю Smalltalk'a не знают?

Годная!

Даешь неделю регулярных выражений на Хабре!

> Автора оригинального текста я уволил бы сразу же, в первую нашу встречу.
Автор оригинального текста не пришел бы к вам на работу.

Многие могут — это и называется отсутствие самокритики.

>… чтобы соблазнить упрямого программиста прочитать его. Что-нибудь типа «Что делать с плохим кодом»…
>… такой же птенец, как и все остальные…

Мне всегда было интересно, как можно легко подвести человека к самокритике. У меня никогда не получалось. Я использовал те же фразы по своей сути, но ваша форма изложения оказалась великолепной.

Браво!

> Если вы находитесь здесь по этой же причине
А я все внимательно прочитал. Спасибо, очень захватывающе.

Читайте коммент. Смысл в swap. Вы темповый объект меняете местами с инициализируемым.

*(тудаже)
> и более чистом коде на «плюсах»
Чище чем на чем интересно?

Коротко и ясно.
Большое спасибо!