Я согласен с тем, что способность программного обеспечения быть сложной - это одновременно сила и исцеление ахиллова сухожилия. Однако у предлагаемых решений есть свои проблемы.
Подход CUSEC / Vimeo великолепен, если вы занимаетесь графической разработкой и можете использовать эту среду в своем окончательном приложении. Эта мгновенная обратная связь весьма ценна. Сегодня хорошие программисты используют разработку через тестирование (TDD). Имея тесты, которые можно быстро запускать во время разработки кода (вместо последующего тестирования), вы получаете быстрый цикл обратной связи в существующей среде разработки. Ключевым моментом здесь является концентрация на скорости обратной связи - не поддавайтесь догматизму, в который попадают некоторые люди, занимающиеся TDD.
Подходы, основанные на моделях, решают одну проблему и создают другие. Любая модель, которую достаточно просто представить на одном листе бумаги, также проста в современном языке программирования. На практике модели становятся настолько сложными, что их невозможно расшифровать, как и плохой код. Другая проблема заключается в том, что генератор модели должен быть идеальным, а получаемый исполняемый файл часто бывает раздутым / медленным. Модели также должны охватывать все, чтобы быть безопаснее, чем рукописный код. Одна из больших проблем в случае с Toyota заключалась в том, что они неправильно обрабатывали переполнение стека. Скорее всего, это упущение, а не ошибка реализации, и вряд ли будет смоделировано по тем же причинам, по которым оно не было закодировано.
Инструменты статического анализа, такие как TLA +, более перспективны, но они требуют, чтобы вы кодировали дважды: один для анализа, а затем производственную версию (в коде). Очевидно, что для сложной распределенной системы, такой как S3, это хорошее вложение. Они также «поняли», что вы должны представлять инструмент таким образом, чтобы программисты понимали его ценность. Большой недостаток в том, что самые сложные системы начинались как простые и постепенно усложнялись. Так что нет очевидного момента, когда вы перестаете делать «улучшения» и переходите к формальным моделям.
Я занимаюсь программированием более 30 лет, и самое большое улучшение моей надежности произошло благодаря TDD. Эти подробные отзывы о тестировании ускоряют начальную разработку и позволяют выявлять проблемы при изменении кода во время обслуживания. Конечно, TDD уже присутствует во всех современных языках программирования; так что никто не разбогатеет, продавая это.
TDD - отличный инструмент, но не полное решение. Что мне действительно нужно, так это разумное программное обеспечение. Я должен быть в состоянии спросить «что вы имеете в виду» и «как вы пришли к такому результату» и получить полезные ответы. Кто-нибудь над этим работает?
