![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
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-бальные землетрясения были бы не только не страшны, но и вообще незаметны". Кстати, методы строительства проникают в софтостроение: аналогией запаса прочности, когда балки тупо берутся в несколько раз толще расчитанных, являются проверки во время выполнения и вообще всякие виртуальные машины.
Но общая идея дошла: для сложных алгоритмов есть смысл проверять базовый алгоритм как он есть на правильность. Отвлекаясь от деталей реализации и отвлекаясь от того, что при реализации могут быть внесены ошибки, искажающие изначальный алгоритм. Но если изначальный базовый алгоритм кривой, то даже при идеальной его реализации результат все равно выйдет кривым (что я и имел возможность неоднократно наблюдать живьем).
Не то что бы оно было удивительно. Я тоже люблю структурировать логику послойно, что вот тут у нас - большая картина, а вот тут, слоем пониже - детали, и слоем еще пониже - еще более детальные детали. Меня страшно раздражают плоские API, где все уровни логики размазаны в один слой и переплетены - в них у меня не хватает внимания, чтобы постоянно расплетать в голове эти взаимодействия.
С другой стороны, если вот так внятно расплести базовые алгоритмы и детали реализации по уровням, может никакого моделирования и не надо, может и так будет сразу видна вся кривизна. По крайней мере, у меня есть такой опыт, когда разберешься в какой-нибудь фигне и оказывается, что она правильно работать никак не может, и проверка подтверждает, что действительно, она и не работает, а просто никто не разбирался и никого это не интересовало.
Заодно прочитал его бумагу про Paxos (который был упомянут как один из алгоритмов, проверенных через TLA+): http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf . Действительно, логично, не то что википедия (но в википедии вообще всё - говно), хотя наверное, можно было бы объяснить еще попроще, менее математично.
Еще один момент с лекции, про её название: что, типа, перед постройкой небоскребов надо рисовать чертежи, в отличие от методов софтостроения. С этой метафорой я совершенно не согласен. На самом деле программы - это чертежи, а небоскребы - то, что программы делают. И если кто-то думает, что в деле рисования чертежей для строительства дела обстоят как-то сильно лучше, то они сильно ошибаются. На самом деле наоборот, если бы дома строились так как пишутся программы, то не "залетевший дятел разрушил бы цивилизацию", а "12-бальные землетрясения были бы не только не страшны, но и вообще незаметны". Кстати, методы строительства проникают в софтостроение: аналогией запаса прочности, когда балки тупо берутся в несколько раз толще расчитанных, являются проверки во время выполнения и вообще всякие виртуальные машины.
