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

[pod_baobabom]

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

Comments

[pod_baobabom]

Coq - это в первую реализация тайп-чекинга в Calculus of Inductive Constructions, предоставляющая ряд инструментов для эффективного построения программ, имеющих конкретные типы (которые, как мы знаем благодаря Карри и Ховарду суть утверждения в интуиционистской логике, а соответствующие им программы -- доказательства).

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

Формализация классической математики в Coq - это в данный момент cutting edge, которым главным образом занимаются лучшие умы Франции под руководством Жоржа Гонтье. С непрерывными дисциплинами там вообще всё пока что в зародыше, хотя какие то вещи уже есть, но это далеко не продакшн. Основные топологические определения закодить должно быть несложно, но непонятно, как проверять их для нетривиальных объектов.

[ext_848993]

Хочу меловую доску, надоели маркерные!

[pod_baobabom]

Идею в этом направлении реализовали в Орхусе. Там у тех, кто theoretical computer science, доски меловые. У практиков - маркерные. Видимо, предполагается, что первые основную работу делают не за компьютером, так что им не нужно часто волноваться о чистоте рук.

"A mathematician is expected to sit at his computer and think" -- Hari Seldon