Разное

Программирование считается инженерной дисциплиной, но уровень надежности конечного продукта очень отличается от результатов работы архитектора или других инженеров. Группа европейских ученых начала работу над математическим аппаратом, который позволит навсегда избавить программы от ошибок. Новая разработка на основе так называемой «теории типов», специальной области теоретической математики, должна произвести настоящую революцию в индустрии программирования.

Работа по совершенствованию программирования, как инженерной дисциплины, ведется в рамках проекта TYPES, одним из координаторов которого является профессор Бенгт Нордстрем (Bengt Nordstrom) из университета Чалмерса (Chalmers University) в Гетеборге, Швеция. В противовес традиционному подходу, когда качество программы проверяется в ходе длительных всесторонних тестов, ученые из проекта TYPES создают такую методику разработки, которая с самого начала гарантирует, что будущая программа будет делать то, что должна.

В проекте TYPES задействованы специалисты из 15 университетов и исследовательских институтов Европы, а еще 19 академических и промышленных организаций участвуют в программе в качестве ассоциированных участников.

Новая методика описывает задачу, которую должна выполнять программа, в виде математической теоремы. В рамках проекта TYPES также создаются открытые программные продукты, которые способны выполнять роль «проверяющих редакторов» (proof editors). Согласно теории типов, эти «проверяющие редакторы» являются гарантией правильности алгоритмов.

Может ли абстрактная математическая дисциплина обеспечить высокое качество программ на практике? Европейская математическая школа является одной из сильнейших в мире, поэтому сотрудничество теоретиков и практиков, как убеждены участники проекта TYPES, должно вывести программирование на новый уровень.

physorg.com.

Что-то мне кажется что сложные алгоритмы поведения этим программам будут не по зубам...

+1 до инскуственного интелекта, я не вижу смысла в этом...

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

Если речь только о классических алгоритмах, нам от этого ни тепло, ни жарко будет, так как прикладники работают в массе своей со готовыми сверхнадежными библиотеками.

В общем не очень понятно какой тип ошибок пытаются исключить.

Ну видимо ситуация такая же:

Серега сказал, что настоящие программеры так не поступают. Настоящие программеры, заявил Серега, существа крайне ленивые, поэтому быстренько создают программу, чтобы она сделала все за них, а список загоняют в комп через сканер. С этими словами он засел, как он выразился, "ваять программулю", которая сама будет брать данные из списка, а затем распечатывать готовые приглашения.

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

Все баги Серега выловил часа за четыре, потянулся и сказал, что приглашения можно уже вставлять в принтер. Принтер немного подумал, после чего выплюнул совершенно пустую открытку. Оказалось, как радостно заявил Серега, он забыл обнулить каунтер.

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

Ремарка Видимо, что поиск багов программером, это уже "ламерство", и будет лучше, если ВСЕ поручить компьютеру.)

:)
Записки невесты программиста, А. Экслер?

Ну чьей же еще, не моей "невесты", это точно.))

:)
Я про название книжки и автора

>В общем не очень понятно какой тип ошибок пытаются исключить.
Пытаются получить грант, а не исключить какой-то тип ошибок :)
"В проекте TYPES задействованы специалисты из 15 университетов и исследовательских институтов Европы, а еще 19 академических и промышленных организаций участвуют в программе в качестве ассоциированных участников."
Это ж сколько денег :)

Не обратил внимание :))), вот что значит оторвался от научной среды. Действительно, с формальной точки зрения, а в грантах только она играет наиважнейшую роль, идеальные условия для получения крупного европейского гранта (не будем показывать пальцами, какого :).

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

Если б так было, не рушились бы дома... Это я не только про РФ. Люди - везде люди, и всегда могут сделать ошибку. Те же японцы недавно отозвали всю партию своих машин (не помню какая марка) обратно...
Другое дело, что у архитекторов тех же, насколько я с некоторыми из них знаком, более высокий уровень критичности именно к самим себе. Потому что они понимают цену своей потенциальной ошибки. Сотни человек под обломками дома это тебе не критический сбой в программе... Посему архитекторы сами за собой все расчеты по сто раз проверят, и других попросят. А программисты, в большинстве, если чего-то накосячат, ну максимум - денег не получат. Поэтому и пишут зачастую левой лапой в пьяный понедельник... Но когда им ставится задача крайне серьезного масштаба - они очень сильно начинают смахивать на архитекторов :)

Архитектуре многие тысячи лет и занятие это дорогое - отсюда и критичность к себе. Программированию - несколько десятков лет, программа стоит напорядок дешевле дома и редко приводит к гибели людей или какому-то ущербу - отсюда некритичность, взятся ей не от куда. Отсюда "грязный подход" в каждом втором проекте (т.е. построим, сломаем, сделаем выводы, построим сломаем, сделаем выводы), применяющийся в архитектуре лишь в самых крайних случаях.

Подавляющее большинство из существующих программистов - очень молоды и не имеют инженерного опыта, а старые программисты не задерживаются или не всегда могут применить опыт из-за стремительной эволюции IT-области. Ситуация слишком уникальная из-за закона Мура. Если бы так строй-материалы дешевели - в строительстве бы караул что творилось бы. Шутка Экслера Если бы программисты строили дома, как раз описывает менталитет некритичных к себе людей в строительстве.