Пятничное утро
Оказывается, livejournal глючит при показе медиа в постинге. Презентация про стандарты описания организаций из моего предыдущего постинга у меня в браузере регулярно заменяется роликом проекта Natal, который я опубликовал еще несколько дней назад.
* * *
Обзорчик программ для DSM (design structure matrix) со скриншотами: http://puln.livejournal.com/1790.html

Как я понимаю, puln и дальше будет писать на эти темы.
* * *
Интервью с сэром Tony Hoare (автором Quicksort, Hoare logic, Communication Sequential Processes и вдохновителем языка Occam) -- http://www.infoq.com/interviews/tony-hoare-qcon-interview. В 1999 году он из Оксфордского университета уволился "на пенсию" в Microsoft Research в Кембридже.

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

Полная для меня неожиданность: он имеет базовое образование в греческих и латинских языках, а компьютерную науку и языки учил в МГУ! И целый год участвовал в проекте по машинному переводу "научного русского" на английский. Первая научная статья Tony Hoare была подана и опубликована в русскоязычном журнале "Машинный перевод", он напечатал ее на русскоязычной пишущей машинке друга. Но ему не давали посмотреть на русские компьютеры, они тогда были секретны!