ПО без ошибок

Источник-то каков...

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

Патч к .NET ваяют, что рост моска разработчикам стимулировать будет, картинками непотребными?

эти цели преследуют почти все методы разработки программногообеспечения

Ничего у них не получится. Самые долгоживущие ошибки в программах возникают из-за следующих причин:

1) Исходная нечеткая постановка задачи

2) Предположения, ставшие неверными (например, до введения UTF-8 str++ можно было использовать для перехода к следующему символу, а сейчас нельзя)

3) Бюрократический футбол, когда непонятно, кто виноват, и обе стороны сваливают ответственность друг на друга

4) Простое "забивание" на проблему разработчиками

Ничего для борьбы с этими причинами не делается. И вообще вся эта наука о НАПИСАНИИ программ без ошибок сама по себе бесполезна и должна быть дополнена наукой о НЕВНЕСЕНИИ ошибок в ходе развития программы.

Окаменелый боян это. Уже есть такие методики, только они охренетительно дорогие.

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

А ссылок можно подкинуть?

Лучше киньте ссылку на книжку о том как Кнут ТеХ отлаживал.

> И вообще вся эта наука о НАПИСАНИИ программ без ошибок сама по себе бесполезна и должна быть дополнена наукой о НЕВНЕСЕНИИ ошибок в ходе развития программы.

+1. И не только в ходе развития, но ещё в ходе проектирования. И всё равно один хрен от человеческого фактора, способного изг..нять любую математику и формализации, никуда не денешься.

>И не только в ходе развития, но ещё в ходе проектирования.

Водопадом пользуются только студенты.

http://www.cs.toronto.edu/~hehner/wrong.pdf + обрати внимание на библиографию.

> ученые из проекта TYPES создают такую методику разработки, которая с самого начала гарантирует, что будущая программа будет делать то, что должна.

-- А где моя зелёная кнопочка?! Вот, тут была! Как это "теперь жёлтенькая"?!... А где зелёненькая?

:-)

> будущая программа будет делать то, что должна.

о каких программах идет речь?

> А где моя зелёная кнопочка?!

Не так. Постановщик описывает задачу: "хочу что бы кнопочка была зимой синего цвета, а на восходе - фиолетового". Вот это вот ПО должно отловить как пинимум две проблемы в постановке задачи: во-первых не определён дефолтный цвет, а во вторых существует конфликт в требованиях к цвету кнопочки зимой на рассвете. Любой нормальный программист не стал бы заморачивать клиента такой ботвой и сделал бы по своему усмотрению, а программа не позволит вносить неоднозначности в спецификацию.

> http://www.cs.toronto.edu/~hehner/wrong.pdf + обрати внимание на библиографию

+ найди ошибку в доказательстве про x+1 (она есть)

ученым просто скучно :-)

Гёделя им надо читать. Думаю, что дальше FP они не пойдут. А вообще это пахнет каким-то диким освоением чьих-то бюджетных денег. "Нанотехнологии в создании безошибочного ПО. Корпорация -РосОшибки-".

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

Осспади, очередные британские учёные. Доказывать софт как теорему придумали ещё тыщщу лет назад. И тогда же прикинули, насколько это затратно.

Всё, что они могут создать - это некоторую автоматизированную систему проверки. Да и того, поди, не будет.

Узок круг их интересов. Страшно далеки они от народа.

Когда-то давно я про подобную технику разработки уже читал. http://en.wikipedia.org/wiki/Cleanroom_Software_Engineering