kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

Мирное сияние чистого разума

Вот Воеводский и ко - Унивалентные основания математики - что казалось бы может быть оторванее от жизни и мирнее.

Собственно сам так думал - "Впрочем, теперь, когда сведения мои пополнились" (© "Сердце тьмы") я бы насторожился уже при фразе "идея использования интуиционистской теории типов Пера Мартин-Лёфа", после же упоминания "В феврале 2010 года Воеводский начал создавать библиотеку на Coq..." - у меня в голове начинает играть военная музыка :)))

Потом опять окажется что все это прибрало под себя министерство обороны с боингом и аэробусом :)))

Cобственно - иллюстрация к той старой истории в MIT AI Labs: http://kouzdra.livejournal.com/3007623.html

PS: Как там в фашистском Мюнхаузене:
https://youtu.be/w2It3PCRiUo?t=4753

- The wind is still unfavourable, Your Excellency
But as soon as it changes, I'll be ready for the ascent

- Monsieur Blanchard, I welcome your intended flight

- We serve science and amuse the people

- It's part of a statesman's art to do
one thing and achieve two

- I serve only science

- Retain that superstition; it is a card in our hand

:)
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 37 comments