juan_gandhi | дыбр

Сегодня с утречка всем на работе впариваю нашу птичку; народ как-то поразительно медленно въезжает, пока живую картинку не покажешь, глядят мутными глазами - зато потом визжать начинают.

В пятницу Шенщон обнаружил (или, более вероятно, получил в мейле из Китая) ексепшен в моём джаре. Ексепшен такой, что, дескать, класс не грузится. В пятницу же вечером он послал этот мейл Дэвиду. Дэвид в понедельник днём перепослал мне это дело, с лаконичным предложением разобраться. Я почту читаю утром и вечером, а днём работаю. Так что прочитал вечером.

С утречка был долгий разговор с Весом, как вообще можно что-то улучшить в этой конторе; потом, после всякой там канцелярской деятельности, пошел у Ирины попросил андроида, посмотреть на живом девайсе, что там не работает. Выдала она мне андроид; оказался не андроид, а андроидоид - к нему нужен ещё специальный драйвер, после чего он детектируется и пускает в шелл. Но апликации не грузит (зависает).

В обед съездили с Женей в Маунтин Вью, поели борща и жареной рыбы в гонконгском ресторане. да поговорили за жизнь. Женя триатлон бегал, сильный мужик, э.

А после обеда пошел уже с Дэвидом в уголок, где сидят эти люди, которые мой джар к своей апликации цепляют. Шенщон сидит спиной, в процесс не вступает - типа он ни при чём вообще. Дэвид дал мне андроида - опять андроидоида, от Моторолы, с неизвестной версией неизвестно чего. Я компилировал всё для 2.0, т.к. CDMA надо включать; а им, оказывается, надо, чтобы версию 1.6 тоже поддерживал. Где CDMA нету. Интересная новость, аккурат перед релизом.

Так что я пошел к себе, стал рисовать хитрый эклипсовый проект, с уже известными фокусами типа "если класс чего-то не загрузился, значит, придётся без него". Кстати, андроидоида-то мне не дали, самим нужен. Контора экономит 300 баксов, хотя бы и с риском задержки релиза. Да они не только на андроидах, они и на карандашах экономят.

Ну мне-то пофиг; я в 6 снялся и поехал в КаЧинг, подписал офер. Как-то неудобно даже, меня там приветствуют как селебрити, подходят и хвалят джавный опшен (надо ещё блогинку написать про это дело). Ну надеюсь и я им полезен буду. Вчера с ними ужинали как раз примерно на цену того андроида, в модном греческом ресторане в Пало Альто.

Но рассусоливать мне некогда, т.к. надо было в Стэнфорд, в библиотеку, читать Мартина-Лёфа, Интуиционистскую Теорию Типов. Миленькая книжечка, написана популярным языком, и как-то подозрительно наивно. Ну то есть, строго пересказать всё эту параферналию в семантике Крипке-Жуаяля раз плюнуть; я только сомневаюсь, что так уж "аксиома выбора" будет доказуема; сдаётся мне, что его интуиционизм и состоит в неявном принятии аксиомы выбора ещё в основаниях - а потом её же доказываем.

Ну это ладно. Прочитал это дело; ясности прибавилось не очень много, но как-то взгляд упростился. И пошел посмотреть, что там ещё есть из логики. Вдруг бац:

Алгоритмы в современной математике и её приложениях (чч 1, 2)
ВЦ СОАН, Новосиб 1982
под ред А.П.Ершова и Д.Кнута"

Вот содержание второго тома:

Манин, Расширяющая конструктивная вселенная
Ван Вейнгаарден, Безъязыковое программирование
Непейвода, Логический подход к программированию
Тыугу, Структурный синтез программ
Летичевский, О поиске инвариантных соотношений в программах
Адельсон-Вельский, Слисенко, Что мы можем сделать с задачами полного перебора
Альдер, Штрассен, Алгоритмическая сложность линейных алгебр
Клини, Алгоритмы в различных смыслах
Шанин, Роль понятия алгорифма в семантике арифметических языков
Цейтин, От логицизма к процедурализму
Ершов, Абстрактная вычислимость в алгебраических системах
Бауэр, Алгоритмы и алгебра
Глушков, О формальных преобрахованиях алгоритмов
Матиясевич, Что делать после установления неразрешимости алгорифмической проблемы
Буда, Об опыте езды на двух конях в программировании
Анисимов, Преобразование Чёрча-Россера и разрешимые свойства обработки деревьев
Клини, Об истоках теории рекурсивных функций

Клини там выглядит очень странно - фактически, обсуждает выступления предыдущих ораторов, каждому или возражая, или поддакивая.