?

Log in

Previous Entry | Next Entry

Будни НИИЧАВО

Недавно я осознал, что не знаю, как правильно называть свою профессию по-русски. По сути, postdoctoral researcher -- это такая промежуточная стадия между аспирантом и профессором (которая вполне может затянуться лет эдак на шесть в особо запущенных случаях). Разумеется, гениальный Jorge Cham и про это комикс нарисовал.

В русском языке слово "постдок" присутствует, но не очень распространено, а называть себя исследователем или учёным у меня не поворачивается язык. В моём понимании учёный -- это такой доктор Гаспар Арнери из сказки "Три Толстяка". Исследователь же - это, скорее, что-то прикладное и экспериментальное, с результатами очевидной полезности, такими как leap motion, к примеру. Уменьшение потребления памяти программами, скомпилированными GHC, или доказательство теорем в Coq, несомненно, тоже делает делает чью-то жизнь приятнее, вот только желаемого wow-эффекта не даёт.

Руководство нашего института это понимает как никто другой, в связи с чем, по случаю официального открытия нашего здания месяц назад, был куплен девайс первоочередной необходимости - композитный сенсорный дисплей. Выглядит чудо техники вот так:

screen1

Если провести по дисплею рукой, можно почувствовать себя Нео, агентом Смитом и Томом Крузом из Minority Report в одном лице. Никогда ещё игра в Space Invaders не была такой увлекательной.

screen2

Бенефис моего начальства перед чудо-агрегатом (на 37-й секунде видео) длился ровно 10 секнуд, после чего губернатор Мадрида отогнал его и на радость журналистам начал бодро тыкать в экран, лично убедившись, что люди здесь занимаются серьёзным и полезным делом.



Сенсорная панель -- 48000 евро по карте MasterCard (именно так, с тремя нулями). Репутация -- бесценна. Эффект достигнут, гранты одобрены, а потревоженные гики снова могут вернуться к маранию маркерных досок.

Comments

( 5 comments — Leave a comment )
itman
Aug. 15th, 2013 12:41 am (UTC)
А знает ли Coq, например, про всякие штуки вроде компактности пространств или он только оперирует простыми assertions?
pod_baobabom
Aug. 15th, 2013 01:40 pm (UTC)
Coq - это в первую реализация тайп-чекинга в Calculus of Inductive Constructions, предоставляющая ряд инструментов для эффективного построения программ, имеющих конкретные типы (которые, как мы знаем благодаря Карри и Ховарду суть утверждения в интуиционистской логике, а соответствующие им программы -- доказательства).

Лучше всего такой подход используется для работы с (ко-)индуктивными предикатами и типами данных. По счастью, таковыми описывается практически всё что есть интересного в теории языков программирования: семантики, системы типов, специализированные логики, утверждения о корректности оптимизаций и анализов и т.п..

Формализация классической математики в Coq - это в данный момент cutting edge, которым главным образом занимаются лучшие умы Франции под руководством Жоржа Гонтье. С непрерывными дисциплинами там вообще всё пока что в зародыше, хотя какие то вещи уже есть, но это далеко не продакшн. Основные топологические определения закодить должно быть несложно, но непонятно, как проверять их для нетривиальных объектов.
itman
Aug. 16th, 2013 04:10 pm (UTC)
Понятно, спасибо!
Dmitry Lomov
Aug. 17th, 2013 10:22 am (UTC)
Хочу меловую доску, надоели маркерные!
pod_baobabom
Aug. 17th, 2013 11:16 pm (UTC)
Идею в этом направлении реализовали в Орхусе. Там у тех, кто theoretical computer science, доски меловые. У практиков - маркерные. Видимо, предполагается, что первые основную работу делают не за компьютером, так что им не нужно часто волноваться о чистоте рук.

"A mathematician is expected to sit at his computer and think" -- Hari Seldon
( 5 comments — Leave a comment )