От Ваших выделений (главных мыслей) -- лично у меня просто резь в глазах. А все Ваши сообщения мне напоминают слайды с лекции -- набор тезисов и несвязанных слов, требующих разъяснения и доказательства. Повтор "российские студенты выигрывают олимпиады по программированию" и витиеватый список Ваших званий и должностей таковыми не являются. """были когда-то и мы рысаками""", спорили когда-то и мы с академиками (например, с А.П. Ершовым).
1)
олимпиады
A.Эйнштен писал(а):
лишь теория объясняет, что же мы ухитряемся наблюдать
Давайте рассмотрим альтернативную теорию побед российской команды. Программирование -- дисциплина прикладная. Это не астрофизика, где больших денег не сделать. Хороший программист и в России получает одну-две тысячи долларов, что совсем не плохо, не правда ли. Студента, выигравшего олимпиаду, приглашают западный фирмы на большие деньги -- это я уже Вас цитирую. То есть, начиная заниматься программированием, российский студент понимает, что светлое будущее ему обеспечено. И умные молодые люди идут заниматься программированием, готовяться к олимпиаде и т.п. Не то в Америке. Там образование рассматривается как вклад денег в будущую карьеру. И кто же будет вкладывать 50-150 тысяч доларов в образование в отрасли, которая все больше перемещается в Индию и Россию? Умные идут заниматься молекулярной биологией или физикой. Выигрыш олимпиады не дает американскому студенту практически ничего. Мораль -- вместо подготовки к олимпиаде лучше подготовиться к экзамену. Это -- конкретная отметка, средний бал, шанс найти лучшую работу и выторговать большую зарплату. Вот и побеждают лучшие русские посредственных американцев. Что ровно ничего не говорит о доказательном программировании.
2)
доказательное программирование
Интересно, что в западной литературе термин такой не употребляется. Поэтому было бы социально ценно, если бы Вы дали определение, что такое "доказательное программирование". Желательно также, чтобы из него было бы сразу понятно, чем оно отличается от структурного (в понимании Гриса, Дейкстры и Хоара). Без определения термин -- это пустой звук. Написание же программ, которые можно доказывать -- это отдельная тема. Традиционные языки типа Java или С для этого подходят плохо. Лучше бы конечно, Haskell или Eiffel. На каком из них учат в России? Кстати, исследования по доказательству правильности программ на Западе ведутся, а термин "доказательное программирование" не употребляется -- с чего бы это?
3)
РАЯ и иже с ней
Была такая теория у А.П. Ершова, но большого распространения не получила. Из причин я выделю три. Первая -- почти все приличные программисты худо-бедно читают по-англицки (хотя бы в объеме ОС ЕС). И поэтому запомнить два-три десятка ключевых слов для них не великая проблема. (Пользуемся же мы латинским и греческим алфавитами в математике. И ничего, никто не плачет -- а попробуйте готику от руки на лекциях пописать.
) Вторая -- это циркуляция программ. Если Вы пишете для себя -- нет проблем, пишите хоть на амхарском или тохарском-Б. Если же Вы публикуете программу -- Вам нужно, чтобы Вас поняли носители многих языков. Поэтому я видел очень мало программ на Java с русскими идентификаторами -- хотя язык это позволяет (Java позволяет и такую экзотику, как неарабские цифры.) Третья причина связана непосредственно с особенностями русского языка. Для него характерна флексия, видоизменение слов для согласования. Почему-то многие авторы ЯП об этом забывают. В результате вместо предложений мы имеем поток слов и убогих сокращений (типа УБИСДУ -- УБрать ИСходящие ДУги). Мое мнение -- дохлая эта идея.
4)
фирмы (здесь и там)
Программирование, как уже говорилось, занятие прикладное. Посему фирмы деньги счиатют. Вот и получается, что пока-что доказанная программа стоит в несколько раз дороже. И поэтому доказательство правильности программ применяется там, где это
необходимо. Например, в медицине. А MS доказательством своих программ не занимается -- незачем. Автоматизация же тестирования -- необходимый, но не достаточный инструмент. Я работал с несколькими пакетами IBM в разное время, и багов там хватало. Про MS и говорить-то неинтересно -- как лежал народ под столами корчась от смеха, когда MS объявило, что из-за переполнения счетчика Win95 может повиснуть через 49 дней неперывной работы. Про то, как заставить Win95 проработать 49 дней MS предусмотрительно не сообщал. Были и другие учителя -- например "три кореша" из Rational Software. Народная мудрость рекомендавала сохраняться раз в минуту при использовании их пакетов, чтобы данные не потерять. И работали они с одним типом мыши -- авторам, по-видиммому, было неизвестно о других. Хорошо хоть, не только на компе авторов -- хотя до этого недалеко было. Зато в России -- класс. И программисты классные. Осталось только назвать крупные фирмы и заметные програмные продукты. Я готов назвать две -- Параграф (если еще независим) и ABBYY. Где же работают эти великолепные прораммисты, затыкающие за пояс всех и вся? Похоже, мало правильность программ доказывать. И олимпиады выигрывать. (Между прочим, FineReader признан едва ли не лучшим пакетом OCR -- на Западе. Я знаю и другие удачные примеры. Но их очень и очень мало.)
5)
спецификации
Quis custodiet ipsos custodes? Вы можете говорить, что программа правильна, коли она соотвествует спецификации, но тогда встает вопрос о доказательстве правильности и непротиворечивости спецификации. И как это делать? И что делать, когда спецификация меняется -- а это происходит ежедневно, это нормальная часть живого бизнеса. Меняются законы (государства), меняется оборудование, появляются новые идеи, как больше продать -- и что же, ждать по году, теряя деньги? Между прочим, я умею из условия вывести программу (доказательно), но так и не понял, как из спецификации доказательно вывести структуру объектов системы. Или алгоритм. Так что спецификация, опять-таки, необходимый но не достаточный инструмент. И еще -- как Вы думаете, что Вам скажет клиент, если программа работает не так, как ему надо, а Вы ему покажете спецификацию? Пошлет Вас вместе со спецификацией... в лучшем случае -- переделывать программу. И у Вас будет четкий и недвусмысленный выбор -- переделать или забыть об этом клиенте (и многих других клиентах, любят, заразы, общаться) навсегда. """А вы толкуете о четвертом измерении"""
Можно, можно написть программу свободную от ошибок, конечно, если не учитывать за ошибки сам код (кто-то даже денег предлогал, если програма проанализированная их анализатором окажется идиальной), в смысле - рельную прогу, и вероятность ошибки свести к ничтожно малой величине, т.е. свести её в разряд теоретических. Речь идёт именно о программной реализации, а не о способе трансляции алгоритма системой.
