Я вошел в тройку!

А я и не знал, что в интернете твою цитату могут с легкостью подхватить и расплодить миллиард ее экземпляров.
Одна такая моя заняла третье место :)

Теорема Евклида о простых числах на Agda

Прочитал недавно в книге С. Клини "Введение в метаматематику" о теореме Евклида, которая говорит, что простых чисел существует бесконечное количество. Теорема эта доказывается так же и в интуиционистской логике. Это и послужило стимулом реализовать его на Agda.

Почему вместо exist пишут forall?

А вот почему...
Читал  сегодня про экзистенциальные типы. Там автор пишет, что мол нам надо exist, а мы пишем forall, но они эквивалентны и это легко доказывается. Но доказательства автор не привел, а поскольку я сижу сейчас на интуиционистской логике и Агде, решил доказать, и поскольку доказательство ну очень простое решил, что все должны его знать.

[Ссылки] Верифицированный QuickSort на Agda

(Копипастить не буду, но держать в одном месте все же лучше.)

Прочитав несколько книг по типизированному лямбда исчислению, а именно по зависимым типам, увидел интересную закономерность: везде первым примером приводится определение типа «отсортированный список». Все бы хорошо, но дальше этого определения ничего не было. Вот я и придумал восполнить этот пробел и реализовать функцию, принимающую список, и возвращающую другой список и два доказательства. Одно доказывает, что результат — это перестановка входа, а другое доказывает, что результат — отсортированный список.
Читать далее [Habrahabr]  

[Ссылки] Самый правильный безопасный printf

(Копипастить не буду, но держать в одном месте все же лучше.)

Под катом Вас ждет увлекательная история о том, как я сильно расстроился, познакомившись поближе с пользовательскими литералами (с нового стандарта), но при этом в последствии все же реализовал вышеупомянутую функцию, а также разобрался с constexpr, а позже еще и реабилитировал те самые литералы
Читать далее [Habrahabr] 

[Ссылки] C++ Variadic templates. Каррирование и частичное применение

(Копипастить не буду, но держать в одном месте все же лучше.)

Доброго времени суток, уважаемое Хабрасообщество.
Недавно приходилось наблюдать дискуссию о каррировании и частичном применении. Суть этой полемики состояла в том, что лучше, для практических целей, иметь в языке программирования: встроенное частичное применение (например, как в Nemerle) или встроенное каррирование (как, например, в Haskell). 
Читать далее [Habrahabr]

Парней с Microsoft тянет на Linux?

Попался как то на глаза язык F*. Интересен он тем, что с зависимыми типами, еще более интересен, что разрабатывается Microsoft Research, но еще более интересно, что парни там умные, и хоть используют, но все же не чистый Windows: не сложно заметить в архиве с исходниками файлик setenv.sh, описание к которому следующее: "A Cygwin bash script to add FSTAR_HOME to your environment".
Вывод: все люди, все все понимают, но политика есть политика.