Лампорт

[sab123]

Прослушал нынче лекцию Лесли Лампорта, который в этом году получил премию Тьюринга. Лекция была про TLA+, и из нее было напрочь непонятно, что именно оно делает. Чего-то как-то моделирует согласно правилам переходов между состояниями, но как именно - непонятно. Надо будет собраться почитать тут: http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

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

Не то что бы оно было удивительно. Я тоже люблю структурировать логику послойно, что вот тут у нас - большая картина, а вот тут, слоем пониже - детали, и слоем еще пониже - еще более детальные детали. Меня страшно раздражают плоские API, где все уровни логики размазаны в один слой и переплетены - в них у меня не хватает внимания, чтобы постоянно расплетать в голове эти взаимодействия.

С другой стороны, если вот так внятно расплести базовые алгоритмы и детали реализации по уровням, может никакого моделирования и не надо, может и так будет сразу видна вся кривизна. По крайней мере, у меня есть такой опыт, когда разберешься в какой-нибудь фигне и оказывается, что она правильно работать никак не может, и проверка подтверждает, что действительно, она и не работает, а просто никто не разбирался и никого это не интересовало.

Заодно прочитал его бумагу про Paxos (который был упомянут как один из алгоритмов, проверенных через TLA+): http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf . Действительно, логично, не то что википедия (но в википедии вообще всё - говно), хотя наверное, можно было бы объяснить еще попроще, менее математично.

Еще один момент с лекции, про её название: что, типа, перед постройкой небоскребов надо рисовать чертежи, в отличие от методов софтостроения. С этой метафорой я совершенно не согласен. На самом деле программы - это чертежи, а небоскребы - то, что программы делают. И если кто-то думает, что в деле рисования чертежей для строительства дела обстоят как-то сильно лучше, то они сильно ошибаются. На самом деле наоборот, если бы дома строились так как пишутся программы, то не "залетевший дятел разрушил бы цивилизацию", а "12-бальные землетрясения были бы не только не страшны, но и вообще незаметны". Кстати, методы строительства проникают в софтостроение: аналогией запаса прочности, когда балки тупо берутся в несколько раз толще расчитанных, являются проверки во время выполнения и вообще всякие виртуальные машины.

Comments

[anspa.livejournal.com]

Серег, а можешь такое же типа на английском писать? Помнишь, говорили..

[sab123.livejournal.com]

Могу, надо будет найти, у меня те ссылки еще есть :-). Кстати, из недавнего: http://babkin-cep.blogspot.com/2014/03/automatic-views-for-normalized-databases.html . Могу перепостить.

[vit-r.livejournal.com]

Пардон, но строительство - это не "рисование чертежей", а дофига работы, включая построение моделей и расчёты.

[sab123.livejournal.com]

Расчеты - вещь шаблонная. В этом смысле тестирование софтвера покрывает расчеты мостов как бык овцу. Часть, требующая интеллекта - это рисование чертежей (т.е. знание, что нарисовать).

[anspa.livejournal.com]

Ага, было б классно. Я тебе на верайзон ответил, получил?

[real-big-shish.livejournal.com]

Более того, нынче здания сначала пишутся на языке AUTOLISP :)

[vit-r.livejournal.com]

Ну как же покрывает, если после тестирования остаётся масса ошибок?

А интеллект снижается по цепочке архитектор - инженер-строитель - чертёжник. Кто именно имеется ввиду под "рисованием чертежей" и видел ли благородный дон работу архитекторов или инженеров-строителей вживую (то есть в процессе или хотя бы в промежуточных результатах)?

[sab123.livejournal.com]

Не надо думать, что после расчетов ошибок не остается. На эту тему мне очень нравится история про спроектированный Ф. Л. Райтом дом "Falling Water". Когда его стали строить, подрядчик сказал "балки на крыше как они спроектированы делать нельзя, они сразу развалятся" и положил балки втрое толще. Архитектор очень скандалил, но было уже поздно, балки положены. Однако позднее оказалось, что и втрое толще было все равно недостаточно, через несколько лет крыша просела. Или вот из недавнего: сотрудник решил перестроить кухню. Специально заказанные окна сделали на полтора дюйма шире, чем место, куда их можно поставить.

По рисованием чертежей имеется в виду архитектурная контора в целом. Чертежник не рисует чертежи, а только копирует.

[vit-r.livejournal.com]

Процесс нельзя объяснять результатом.

В принципе, я видел как индусы считают кабеля на подводной лодке. Это не значит, что у белых инженеров они тоже гореть будут.

[sab123.livejournal.com]

Угу.

[sab123.livejournal.com]

Вот прям так здания? Или тулзы для рисования зданий?

[sab123.livejournal.com]

Ну так горят же. И падают. А чтоб падали поменьше, используют принцип запаса прочности, когда каждый элемент делают в несколько раз толще расчитанного.

На эту тему у меня есть история про Боинг. В 30-е годы Сиэттл мог наблюдать первый полет новой летающей лодки Боинга. Которая взлетела с озера, сделала охренительных размеров круг, и приземлилась. Круг такой вышел потому, что хвост оказался маленьким и в аэродинамической тени, и в результате самолет совершенно не управлялся рулем направления. Поэтому пилотам пришлось кое-как разворачиваться другими подручными средствами.

[vit-r.livejournal.com]

Пардон, с тридцатых годов стоимость расчётов и их возможности изменились на порядок. Это только программисты до сих пор ваяют всё напильником на коленке.

[sab123.livejournal.com]

Это не те расчеты. С 30-х годов изменились возможность моделирования. Когда вместо строительства реального самолета строят его модель и проводят через имитацию полета. Модель сама по себе не говорит, какой именно надо делать хвост. Модель говорит, что имеющийся в проекте хвост малоэффективен. Ну так в программировании то же самое называется тестами: прогон программы на имитации данных и сравнение созданных ей результатов с ожидаемыми. Точно так же тесты не говорят, что именно и как именно в программе надо изменить, чтобы результаты стали правильными. Они говорят только о том, что результаты неправильные.

[vit-r.livejournal.com]

Ой, сейчас мы начнём говорить про покрытие тестов.

Ладно, ухожу, ухожу.

[sab123.livejournal.com]

И с покрытием тестов - совершенно та же самая фигня. Например, при эксплуатации транспортных самолетов C-5 Внезапно выяснилось, что у них со временем трескаются балки крыла. Налицо пробел в тестовом покрытии.

[real-big-shish.livejournal.com]

Ну, чертежи. И не только рисования, там же моделирование и анализ. А тулза - Автокад.

[sab123.livejournal.com]

Про тулзу я в курсе. Но живой-то же человек вроде только чертежи чертит, а не Лисп пишет?

[real-big-shish.livejournal.com]

Ну, если тот человек как спец полужив, то в ручную мышкой по-дедовски. А если спец подготовленный, то сразу пишет на Лиспе, так раза в два-три быстрее, и ошибок втрое меньше.