Top.Mail.Ru
? ?
kouzdra [entries|archive|friends|userinfo]
kouzdra

[ website | www.kouzdra.org ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Мирное сияние чистого разума [Jun. 11th, 2016|07:08 am]
kouzdra
Вот Воеводский и ко - Унивалентные основания математики - что казалось бы может быть оторванее от жизни и мирнее.

Собственно сам так думал - "Впрочем, теперь, когда сведения мои пополнились" (© "Сердце тьмы") я бы насторожился уже при фразе "идея использования интуиционистской теории типов Пера Мартин-Лёфа", после же упоминания "В феврале 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

:)
LinkReply

Comments:
From: (Anonymous)
2016-06-11 05:05 am (UTC)
Главное, чтобы в МО находились эксперты, которые отличают потенциально перспективные технологии, от "петрика", дабы затраты оптимизировать и зерно не упустить. В случае с Воеводским эта задача выглядит достаточно прозрачной.
(Reply) (Thread)
[User Picture]From: kouzdra
2016-06-11 05:08 am (UTC)
А экспертов никаких не будет - просто с приличной вероятностью прикладные инженеры приспособят его труды для решения вполне прикладных задач и все - Воеводскому об это скорее всего даже и говорить не будут.

Другое дело, что сейчас-то мог бы и сам догадаться где наиболее вероятное практическое применение его штудий находится

Edited at 2016-06-11 05:15 am (UTC)
(Reply) (Parent) (Thread)
From: (Anonymous)
2016-06-11 05:18 am (UTC)
Знаете же, что значительная часть "самых разрушительных технологий" изначальная военкой финансировалась, почти что от самого их зарождения (ну, может быть, чуть позднее). Затратное же это все дело, чтобы какие-то частные фонды это тянули, а госка это всегда военка, эквивалентные понятия по сути, что бы при это ни говорили.
(Reply) (Parent) (Thread)
From: aso
2016-06-11 10:00 am (UTC)
Знаете же, что значительная часть "самых разрушительных технологий" изначальная военкой финансировалась, почти что от самого их зарождени

Если мы про ядерное и термоядерное оружие - то оно финансировалось военными только с этапа "теоретической готовности" - когда, в общем-то, основные научные проблемы квантмеха были разрешены - и остались только инженерные.
"Хайтечно-инженерные", конечно, но, тем не менее...
(Reply) (Parent) (Thread)
[User Picture]From: __gastrit
2016-06-11 05:29 am (UTC)
> приспособят его труды

А что, там открыли принципиально новый тип вычислимости, позволяющий обойти теорему о неполноте?

С уважением,
Гастрит
(Reply) (Parent) (Thread) (Expand)
[User Picture]From: kouzdra
2016-06-11 05:41 am (UTC)
А причем тут теорема о неполноте - просто если окажется, что его формализм удобнее для тех целей, о которых тут последнее время обсуждается (а как я понимаю - HoTT претендует на что-то схожее) - то разумеется его переймут
(Reply) (Parent) (Thread) (Expand)
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
From: (Anonymous)
2016-06-11 10:38 am (UTC)
в МО находились эксперты, которые отличают потенциально перспективные технологии, от "петрика", дабы затраты оптимизировать и зерно не упустить.

Ходят слухи, что советскую военно-лазерную программу "оптимизировали" (нафиг закрыв некоторые направления) именно привлеченные по хоздоговорам вузы. Физфак Казани что ли.
Поскольку военные озвучить несложный факт "пропихнуть через приземную атмосферу, столько, чтобы хватило разрезать броню танка не удастся никак" не осиливали больше 10 лет.
А гражданским что, им звездочки на плечи не капают.
К рейнметалловской машине не относится - она не по танкам, она по авиамоделям.
(Reply) (Parent) (Thread)
From: (Anonymous)
2016-06-11 11:39 am (UTC)
Но рельсовые пушки точно делают, и начали это дело еще в конце 80-х. Не знаю, правда, насколько все это эффективно-)) ИМХО - хунйя. Но пиндосы рекламируют.
(Reply) (Parent) (Thread) (Expand)
(no subject) - (Anonymous) Expand
From: spqr_voldi
2016-06-11 12:36 pm (UTC)
Человек, к этому относившийся, рассказывал, что значительная часть лазерной программы (в объёме небольшого городка) была сугубо для того, чтобы куда-то людей пристроить.
(Reply) (Parent) (Thread)
[User Picture]From: avshap
2016-06-11 10:24 am (UTC)
Моррис обошел вокруг, разглядывая машину.
— Она играет в пинг-понг?
— Довольно плохо, — признался Фарли. — Но мы над ней работаем. Мы получили дотацию от Министерства обороны на робота, играющего в пинг-понг. Я знаю, о чем вы думаете. Вы думаете, что это одно баловство.
Моррис пожал плечами. Ему не нравилось, когда ему то и дело сообщали, о чем он думает.
Фарли улыбнулся:
— Одному богу известно, зачем это им понадобилось. Но, конечно, такой робот открывает массу возможностей. Представьте себе компьютер, способный распознать сферическое тело, быстро перемещающееся в трехмерном пространстве, а затем ударить по этому телу так, чтобы оно отлетело назад в строгом соответствии с определенными правилами. Ведь шарик должен упасть между двумя белыми линиями, обязательно удариться о стол и так далее. Так что вряд ли такой робот требуется им для розыгрышей первенства по пинг-понгу.

(ц)Майкл Крайтон
(Reply) (Thread)
[User Picture]From: os80
2016-06-11 10:25 am (UTC)
А почему Мартин-Лёфа подчеркнули?
(Reply) (Thread)
[User Picture]From: kouzdra
2016-06-11 10:39 am (UTC)
А потому что у всей этой науки про зависимые типы именно оттуда ноги растут :)
(Reply) (Parent) (Thread)
From: (Anonymous)
2016-06-11 10:33 am (UTC)
- I serve only science

И все вспомнили Германа Оберта.
Германия, говорите, 1943 год, говорите.
(Reply) (Thread)
From: spqr_voldi
2016-06-11 12:40 pm (UTC)
А какая разница мирное/военное? Воеводский вроде не хиппи, и пока ему не мешают общаться с воображаемыми друзьями, всем доволен. А от чуть более корректного кода и я бы не отказался (а то та же SAP HANA на ровном месте разваливается).
(Reply) (Thread)
[User Picture]From: semonsemenich
2016-06-11 01:31 pm (UTC)

ОФФ-ТОП

"Мы к Вам, профессор. И вот по какому делу".
А кто такой математик Цфасман? Надысь Советскую Власть зело клеймил...
(Reply) (Thread)