[comp] Провокационное сравнение, однако…

Так и хочется задать несколько вопросов: Ну и почему этими замечательными 8MHz машинами не пользуются сейчас? Почему они не вытесняют тормознутые 1600MHz поделия с рынка? С какого хера вообще нужно такие сравнения проводить? И т.д.

[prog] Прочитал несколько интервью Бертранда Мейера (часть 2)

Очень интересным оказалось интервью Бертранда Мейера “КоммерсантЪ”-у. Особенно вот эта цитата, которая предсказывает судьбу подготовки “самых лучших программистов в мире” (выражение в кавычках мое):

Что касается подготовки программистов в России, по-моему, есть очень большой риск. Сила российской школы программирования — это сила русского образования, особенно математической традиции. Именно благодаря ей русские программисты успешны. Но это заслуга советских и даже дореволюционных традиций образования и науки. Я в последнее время много говорил с коллегами о том, что происходит в российской средней и высшей школе, и мне кажется, это довольно страшно. Мало профессоров, особенно среднего возраста — это катастрофа. Мне кажется, что студенты не так сильно интересуются программированием, как интеллектуальной деятельностью. Для них это изначально инструмент зарабатывания денег. Поэтому они больше интересуются достаточно поверхностными навыками вроде web-дизайна. Просто не понимают, что настоящее серьезное, трудное программирование — это увлекательный труд. Возможно, потому, что нет тех, кто мог бы им это объяснить. И вполне вероятно, что через пять-десять лет вся база, на которой основан успех российской программистской отрасли, разрушится. А больше ничего нет. Исчезновение научной и математической базы — это самый большой риск. Конечно, если говорить об ITMO, СПБГУ, политехе МГУ и еще десятке вузов — там проблем нет. Но в вузах второго ранга, даже хороших, все гораздо проблемнее.

Поскольку у Мейера свежий взгляд со стороны, да еще он более-менее в теме высшего образования в России, то, боюсь, он прав :(

[life.sport.darts] Первые впечатления от дротиков Designer Tungsten Darts 80% 24g

Сегодня таки дождался очередной посылки из Англии, которая добиралась ко мне почти полтора месяца. И стал обладателем на удивление хороших дротиков, которые на PureDarts.co.uk продаются под маркой Designer Tungsten Darts – 80% 24-граммовая модель D47. Чуть-чуть подробностей и фотографий под катом.

[prog] Прочитал несколько интервью Бертранда Мейера (часть 1)

Бертранд Мейер в своем блоге дал ссылки на ряд своих недавних интервью в русскоязычных изданиях. Два из них (в Коммерсанте и в Открытых системах) я прочитал. Интересно. Прежде всего потому, что, на мой взгляд, Бертранд Мейер занимает уникальную позицию – сильно посередине между прикладными разработками и научными исследованиями. И, в какой-то мере, является проводником научных достижений в мир прикладной разработки (хотя на эту тему, вероятно, можно сильно спорить).

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

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

Насколько я понимаю, сейчас можно проводить верификацию программ тремя способами:

1. Статический анализ корректности кода в отсутствии формальных спецификаций. Такой анализ выявляет “тривиальные ошибки” как то: отсутствие возврата значения из функции в какой-то из ветвей, обращения к неинициализированным переменным, потенциальные переполнения при выполнении арифметических операций, выходы за пределы массивов и т.д. Часть этих ошибок выявляют сами компиляторы (например, отсутствие return-ов или выбрасывание исключения, не задекларированного в секции throws в языке Java). Часть вылавливают специализированные статические анализаторы. Главное же в этом способе то, что он способен отыскивать “баги”, но ничего не может сказать о правильности работы кода. Т.е. можно написать программу без багов, которая будет делать совсем не то, что нужно. Например, переводить деньги со счета на счет без предварительной проверки допустимости такой операции (например, отсутствие достаточной суммы на исходном счете).

2. Проверка выполнения контрактов программных компонентов. В первую очередь здесь должна быть упомянута система Design By Contract из языка Eiffel (которую так же пытались сделать в D), а так же разного рода попытки реализовать ее в других языках (в виде специальных комментариев или аннотаций). В принципе, в примитивном виде эта практика реализуется даже в C на основе assert-ов. На мой взгляд, DbC – очень неоднозначная вещь. Имел опыт работы с ней во время изучения Eiffel-я. В чем-то она хороша, в чем-то нет. Как бы то ни было, контракты хорошо подходят для небольших повторно используемых компонент (например, библиотек контейнеров или стандартных алгоритмов), а вот доказательство правильной работы некоторого заточенного под конкретного заказчика приложения с помощью контрактов вряд ли можно сделать.

3. Проверка соответствия программы заранее определенным спецификациям. Т.е. сначала для приложения на каком-то формальном языке формируется точная и полная спецификация, затем на каком-то языке программирования эти спецификации воплощаются в реальный код (вручную или посредством кодогенерации), а затем посредством специализированных инструментов (в первую очередь статических анализаторов, а так же run-time анализаторов и генераторов наборов тестовых данных и воздействий) проверяется соответствие реализации исходной спецификации.

На мой дилетантский взгляд, стоимость и сроки разработки существенно возрастают при использовании средств верификации программ. Причем чем более серьезное (а значит и надежное, качественное) средство используется, тем дороже и длительнее будет разработка (в качестве примера можно вспомнить упомянутый мной когда-то проект Tokeneer, выполненный с использованием SPARK Pro).

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

Мне кажется, что есть более фундаментальные причины, которые не позволяют формальным методам стать стандартной частью разработки ПО в нашей индустрии. При том, что мечты о проникновении формальных методов в массы витают в научной общественности чуть ли не столько же лет, сколько существует промышленная разработка ПО.

Один из очевидных факторов – это полнота и корректность составления исходной спецификации. Но тут лучше слушать не меня, а тех, кто этим вопросом вплотную занимается.

Я же хочу заострить внимание на другом аспекте. Верификация требует, чтобы спецификация (т.е. точный набор критериев для проверки кода) была готова до написания кода. Грубо говоря, чтобы полный набор тестов был сделан еще до разработки программы. И вот здесь уже теория (благие намерения) вступают в противоречия с практикой.

Во-первых, не смотря на то, что в разных методиках (скажем, Test Driven Development) требуется писать тесты до кода, намного, намного чаще делается наоборот. Сначала пишется код, разработчик убеждается, что код делает то, что нужно (делая один или два теста для подтверждения работоспособности кода). И лишь потом приступает к более полному тестированию – проверке граничных условий, некорректных входных данных, отсутствия ресурсов и пр. Причем так делают даже при использовании того же TDD – изначально создавая минимальный набор тестов, показывающих работоспособность кода на тривиальных сценариях. И это неспроста, поскольку есть еще и…

Во-вторых, существует замечательный афоризм: Everything should be built top-down, except the first time (т.е. все нужно разрабатывать сверху-вниз, за исключением самого первого раза). И это очень точно описывает ситуацию с разработкой ПО. Нам ведь не так уж часто приходится делать одно и то же снова и снова. Даже в чем-то похожие задачи все равно различаются в деталях. И начиная что-то делать мы далеко не всегда даже знаем, получится ли что-нибудь или не, а если и получится, то что именно. Если же мы не знаем, что получится на выходе, то как можно заранее покрыть итог нашей работы формальными спецификациями?

На эту тему мне вспоминается случай, который произошел на заре моей профессиональной карьеры. Нужно было сделать отображение векторных картинок в окне с возможностью масштабирования и скролирования. Если бы это был наш формат и если бы мы сами отрисовывали картинку, то дело было простым. Но картинка сохранялась в WMF-файле (Windows Metafile) и отображалась средствами Windows (тогда еще 3.11). Я убил на это дело неделю, выкуривая те крохи документации по Windows API, которые были в моем распоряжении и проделывая по несколько неудачных экспериментов в день. В конце-концов, в состоянии, очень близком к отчаянию, я все-таки смог разобраться с премудростями SetWindowOrg, SetViewportOrg и деталями воспроизведения метафайла – WMF начал масштабироваться и скролироваться.

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

В случае же с формальной верификацией такой свободы, насколько мне представляется, нет. А значит и драйва, который разработчик иногда получает от программирования, тоже нет :( А какой же тогда смысл в программировании, если нет кайфа и драйва? ;)

PS. Кстати, в разработке прикладного ПО есть немалая доля субъективизма. Вот тоже отображение метафайла средствами ОС – как формально специфицировать корректность этого отображения? А ведь разработчик просто взглянув на картинку в состоянии точно дать ответ – правильно она отображена или нет. Если же взять такой пласт проблем, как расположение органов управления в диалоговых окнах, их цвета и размеры, моменты замораживания/размораживания и пр. составные части usabillity…

[life.sport.darts] Закончился Чемпионат Мира по версии PDC

Сегодня поздно ночью закончился PDC-шный Чемпионат Мира по дартс. В финале Адриан Льюс со скрипом одолел Энди Хамильтона и стал 2-х кратным чемпионом, защитив свой прошлогодний титул. При этом он оказался всего лишь третьим человеком в истории дартса, которому удалось сделать это (ранее это получилось только у Эрика Бристоу и Раймонда ван Барнивельда).

Смотреть этот чемпионат было сложнее, чем прошлогодний. Беларусь вместе с Россией в этом году не возвращалась на зимнее время, тогда как весь нормальный мир, включая Великобританию, сделали это. Посему разница во времени с Лондоном у нас сейчас 3 часа, вместо 2-х. И матчи, которые начинались поздно вечером в Лондоне, шли у нас уже ночью. Из-за чего ряд интереснейших матчей посмотреть не удалось.

На этом чемпионате я болел за троих игроков – Фила Тейлора (рассчитывая, что он сможет взять 16-тый титул), Дейва Чизнелла (который перешел в PDC в самом начале 2011-го года) и Саймона Витлока (который до Чемпионата два месяца вообще не играл после перелома ноги).

Но расклад матчей оказался неудачным для моих фаворитов – они все должны были бы встретиться между собой еще до финала. Фил Тейлор сыграл с Чизнеллом уже в 1/16. И сенсационно проиграл 1-4. Именно такого исхода и боялся. Дело в том, что Тейлор провел очень хороший сезон 2011-го года – он выиграл Players Championship Finals 2010, World Matchplay, European Championship, World Grand Prix и Grand Slam of Darts. Но затем в его игре наступил явный спад – это очень хорошо было видно в матче с Мервином Кингом на Players Championship Finals 2011 за неделю до Чемпионата Мира. Этим спадом и смог воспользоваться Дэйв Чизнелл, отлично настроившись на один единственный важнейший матч.

После своей сенсационной победы Чизнелл не смог придти в себя и слил вчистую следующий матч Энди Хамильтону – 0-4.

Дольше всех продержался Саймон Витлок, хотя ему было труднее всего – играл он сильно прихрамывая. Более того, в первый день он смог разминаться перед своим матчем всего десять минут – настолько сильно болела сломанная нога. Тем не менее, по ходу чемпионата Витлок собрал приличную коллекцию скальпов – Стива Битона, Майкла ван Гервена и, самый почетный, Гари Андерсона.

Но после Андресона Витлок в полуфинале вышел на Энди Хамильтона. И это был первый из двух сумасшедших полуфиналов этого чемпионата. Фоном к матчу Витлок-Хамильтон был уникальный четвертьфинал летнего World Matchplay, когда проигрывая 8-15 в матче до 16 побед Хамильтон совершил чудо и выиграв 9 легов подряд уделал Витлока 17-15. К сожалению для меня почти то же самое произошло и сейчас. Сначала Хамильтон вышел вперед 3-1, затем Витлок смог переломить ход игры и стал лидировать 5-3. Но Хамильтон не сдался и довел сначала до 5-5, а затем и до 6-5 в свою пользу (последний сет завершился со счетом 4-2). Ключом к победе Хамильтона стали удачные завершения – 58% успешных попаданий в удвоения. Тогда как Витлок, не смотря на отличные наборы (14 максимумов, 34 раза 140+ и 53 раза 100+) закрывался плохо – только 36%.

Второй полуфинал между Адрианом Льюисом и Джейсом Вэйдом был еще более сумасшедшим. Вэйд быстро повел в счете буквально громя Льюиса, у которого ничего не получалось. И вскоре Вэйд довел игру до счета 5-1 в свою пользу – и это в матче до 6 побед! Казалось, что только чудо может помочь Льюису выиграть. И оно таки произошло!

Случилось сразу две вещи. Первая вполне ожидаемая – у Льюиса полетели максимумы. Это вообще его фирменная черта – большие наборы, здесь он может поспорить даже с Андерсоном. Но в начале игры максимумы у Льюиса не шли. Зато потом полетели, да еще в самые нужные моменты. Вторая вещь была неожиданной – Вэйд стал промахиваться мимо удвоений. В том числе мимо своих любимых D20 и D10. Именно это и решило исход матча. Ну, может еще у Вэйда закончилось действие дозы антидепрессантов, которыми его пичкают дабы удержать от суицидных действий.

В матче Льюиса против Вэйда запомнился самый последний лег. Первым бросал Льюис. После 9 дротиков у каждого из игроков осталось по 161. Но право очередного подхода было у Льюиса – и он вышел и закрыл 161! После этого подхода если у кого-то еще и были сомнения в судьбе титула, то они должны были окончательно развеяться.

Итак, в финале сошлись Льюис и Хамильтон. С одной стороны, каждому из них очень повезло. Хамильтон, на мой взгляд, оказался в финале только благодаря везению и невероятному стечению обстоятельств – в первых двух матчах против испанца Альциноса и голландца ван дер Вурта он едва-едва уцелел. Затем была победа над разобранным после победы над Тейлором Чизнеллом. Затем над бельгийцем Хайбрехтом, который и так прыгнул в два раза выше головы, дойдя до 1/4 финала. Потом встреча с поломанным Витлоком, который накануне играл с Андерсоном. В общем, Фортуна подсовывала Хамильтону игроков в нужных кондициях, а Хамильтон на 100% пользовался стечением обстоятельств.

Путь Льюиса на чемпионате так же начинался со счастливого случая – в первом же матче Льюис должен был проигрывать Найджелу Хейдону. И Хейдон даже несколько раз бросал на матч! Но за Льюиса вступился зрительный зал – такого сильного давления зрителей на игрока я уже давно не видел. Хейдон, вероятно, так же, поэтому справиться с реакцией публики не смог. После Хейдона Льюис шел к финалу весьма уверено, обыграв Тортона, Джонеса и Дженкинса с Вэйдом.

С другой стороны, не смотря на явное благоволение Фортуны, в финале оказались два игрока, которые на этом чемпионате сделали самые реальные заходы на 9-darter. Хамильтон в матче против Альциноса промахнулся 9-тым дротиком мимо D18, а Льюис уже в финале промазал 9-тым мимо D12.

Финал же получился не сильно выразительным. Большое количество маленьких наборов, большое количество промахов по удвоениям, очень явное нервное напряжение обоих игроков из-за которого никто из них не мог найти свою игру. Точнее, это Льюис долго не мог найти свою игру, Хамильтон же играл, имхо, на своем обычном уровне. К тому же лично меня Хамильтон очень быстро задолбал своей манерой поведения – после каждого(!) своего удачного похода (большой набор или выигранный лег) он оборачивался к своей жене и со страшной рожей что-то радостно кричал. А поскольку сидела она где-то за телекамерами, то казалось, что он специально на камеру это делает. В результате спокойно на выходки Хамильтона я реагировать уже не мог ;) Льюис, не смотря на свой молодой возраст, вел себя намного спокойнее и достойнее. Наверное поэтому и победил ;)

Заканчивая рассказ о Чемпионате Мира нельзя не упомянуть о яркой игре двух неанглийских игроков, матчи которых мне удалось посмотреь.

Первый – немец Йохан Артут. В первом круге чемпиона едва-едва не уделавший Гари Андерсона. Причем выигрыш Артута, буде он случиться, был бы очень по делу. Но чего-то чуть-чуть не хватило. Мне кажется, что опыта игры на большой сцене. За счет этого опыта Андерсон смог удержаться. Надеюсь, однако, что Артут еще свое возьмет.

Второй – бельгиец Ким Хайбрехт. Совсем молодой игрок, который внезапно заявил о себе на European Championship этого года, где он сенсационно дошел до 1/4 финала. Призовые деньги за это достижение позволили ему заняться дартсом профессионально. И вот на этом Чемпионате Мира он вновь заявил о себе – 3-0 над Брендоном Доланом, 4-1 над Джеймсом Ричардсоном (который в первом раунде оставил не у дел ван Барнивельда), 4-1 над Полом Николсоном. Последняя победа очень дорогого стоит. Поэтом надеюсь, что Хайбрехт не остановиться на этом. Пора уже англичан в дартсе подвинуть – сначала с помощью голландцев, немцев и бельгийцев, а там и мы подтянемся! ;)