HURD планирует очередной переход на новое ядро.

Обычно не встреваю во flame, но тут сложно удержаться.

Дорогие друзья :-)

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

То, что большинство либо вовсе не знает о средствах контроля качества в программной инженерии, либо знает о тестах и считает что они дают гарантию безупречности при 100%м покрытии, то это лишь проблема современного общества. :-)

Учиться, учиться, и еще раз учиться, как завещал товарищ Ленин. Тесты даже при 100%м покрытии _не дают_ 100%й гарантии безупречности. Поэтому в некоторых известных мне компаниях, занимающихся разработкой критичного к надёжности кода их уже перестали использовать и перешли на другие методики.

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

Вот такая вот она, жЫзнь

> ходил. _спецификацию_ версии 0.8+ видел, мне понравилось. а вот код-то где?

Ну что же дальше еще чуть-чуть не прочитал: язык поставляется только вместе с системой... ;)

Жаль, "горячий финский парень" ушел - еще бы чуть-чуть, и я записался бы в тестеры... :)

>Учиться, учиться, и еще раз учиться, как завещал товарищ Ленин. Тесты даже при 100%м покрытии _не дают_ 100%й гарантии безупречности. Поэтому в некоторых известных мне компаниях, занимающихся разработкой критичного к надёжности кода их уже перестали использовать и перешли на другие методики.

Нет и не будет методов которые бы автоматический проверилибы\доказали код абсолютно без участия человека - теоремму надо еще как то ввести (которую к томуже надо также проверить на правильность). А при инженерном складе ума у 95% девелоперов 100% правильно ввести сможет только компьютер-телепат и то если инженер не ошибаеца в своих мыслях. Иные методики (кстати примеры приведи методик заменяющих тестирование и более надежный) не дают бинарного результата а наваляют варнингов которые также проверить сможет только человек - что в свою очередь даст баги. 100% гарантии безупречности нидаст ничто - потому что с самого начала человек есть.

К сожалению, НЕТ УНИВЕРСАЛЬНОГО АЛГОРИТМА ПРОВЕРКИ ПРОГРАММ. Теорема типа.

Так что мечта останется мечтой. Другое дело, что специальным образом спроектированные языки (где-то видел, что в программе на Haskell компилятор вылавливает до 95% всех ошибок) могут существенно снизить вероятность их появления...

Но большинство программеров - и это отмечено совершенно правильно - смотрят не на правильные, а на быстрые средства программирования.

А беда в том, что область знания "программирование" слишком молода (в лице ее носителей), а они считают, что освоив лепку форм в каком-нибудь Билдере они уже могут считаться программистами.

> А возможность _доказательства_ корректности кода в промышленном масштабе это пока что мечта. И мечтой она остается в том числе потому, что очень до многих горе-программистов не доходит что это и зачем это нужно.

ИМХО, самый большой камень на пути верификации то, что в реальных программах полная спецификация (по которой и ведется доказательство) оказывается очень громоздкой, так что руками за разумное время можно доказать только очень простые куски кода (скажем, построить какой-нибудь хитроумный цикл формально, из инварианта), что я несколько раз и делал. Позволять себе роскошь доказывать более объемные вещи можно лишь тем, у кого это входит в должностные обязанности :-(

Автоматическое доказательство в этом наверное поможет, вот только то, что я о нем знаю, не внушает оптимизма. Если я правильно понял, то такая система верификации, как SPIN, основывает(ла) свои доказательства на переборе пространства состояний, пусть и с отсечением лишнего, но объемном. Те же системы, которые основывают поиск доказательств на теореме Эрбрана, могут работать бесконечно, что ИМХО следует из этой теоремы. Впрочем, я не специалист в ATP, и был бы очень рад, если с тех пор придумали что-то новенькое.

Еще, возможно, поможет функциональный подход --- программы в этом стиле ИМХО ближе к формальным математическим спецификациям, что в ряде случаев сводит доказательство к простому сопоставлению матем. постановки задачи с текстом функциональной программы.

А о взаимоотношениях науки с индустрией ИМХО неплохо написал Роб Пайк в своем докладе:

http://www.cs.bell-labs.com/cm/cs/who/rob/utah2000.pdf

--

SVK

А еще я совсем забыл... Если я не ошибаюсь, известная задача "halting problem", поставленная еще во времена Тьюринга (а может и ним самим --- нет под рукой архива), алгоритмически неразрешима. Так что полностью автоматически доказать корректность программы по некоторым обобщенным утверждениям в общем случае ИМХО невозможно (например, "данная программа никогда не трет память и не зацикливается" --- это, конечно же, не тянет на доказательство корректности, но на практике очень полезно). Но если задать руками "функцию декремента", то почему бы и нет?

--

SVK

Доказывают только то, что код соответствует спецификации, не более того. От ошибок уже в спецификации это не защитит.

Согласен. Серебрянной пули нет и видимо не будет. Но есть тенденция в умах считать серебрянной пулей каждую новую методику.

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

Лично мне кажется, что идея создания (или хотя бы выбора) языка под конкретную задачу может очень положительно влиять на качество софта. Но тут главная проблема - косность мышления. Далеко не всякий готов отказаться от использования везде своего любимого и главное понятного C/C++/Java/Assembler/Python/и т.д.

>От ошибок уже в спецификации это не защитит.

Но можно очень упростить. Борланд или Микросфт состряпают очередную версию билдер, жмакнув на пару фомочек получим спуцификацию. И только линуксойды будут по старинки в vim-е. Программистами называть только тех кто в билдере стряпает спецификации, остальных не знаю как будут называть, наверно их загрузят в биореактор.

Ось на функциональном языке - оригинально. Ц уже действительно как-то поднадоел со своими конструкциями из #@%&-подобных символов, собирающимися разными компиляторами по-разному ;)

Да нет, нормальный это язык, не функциональный.

>>HURD планирует очередной переход на новое ядро

Помнится еще мэтр Танненбаум ругал Линуса за неправильную архитектуру ядра. Вот незадача -то. Ядро от линуса худо бедно пашет, а вот с хууууурдом саапсем плохо.