Здравствуйте, Sinclair, Вы писали:
S>>Так что повторюсь, вы не пожелания и мечты свои — а практику озвучьте. S>Практика перед вами ежедневно. S>1. Верификатор дотнета миллионы раз в день доказывает, что в заданной программе нет ошибок типизации. Чистая математика. S>2. Оптимизаторы запросов в СУБД выполняют трансформации планов запросов для сокращения задействованных ресурсов, сохраняя их семантическую эквивалентность. Чистая математика. S>3. Шедулеры транзакций в СУБД обеспечивают сериализуемость сценариев выполнения, обеспечивая гарантию целостности данных. Чистая математика. S>4. Механизмы журналирования в СУБД обеспечивают восстановление целостности состояния после сбоев. Чистая математика. S>5. Оптимизирующие компиляторы — сплошная математика, с теоремами и прочим. S>Можно продолжать до бесконечности.
А нельзя ли чтонть такое, что было бы практически применимо? А то всё это примеры, как программы решают проблемы программистов, созданные самими же программистами. СУБД, даже если с шедулерами и верификацией типов в налоговую инспекцию не сдашь, да и управлять ракетой тоже не поставишь.
S>А нельзя ли чтонть такое, что было бы практически применимо? А то всё это примеры, как программы решают проблемы программистов, созданные самими же программистами. СУБД, даже если с шедулерами и верификацией типов в налоговую инспекцию не сдашь, да и управлять ракетой тоже не поставишь.
Простите, но я не могу вам ничем помочь. В налоговую вы сдаёте отчёт, подписанный цифровой подписью, основанной на вполне себе конкретной математике. При подготовке этого отчёта вы пользовались СУБД, построенной на основе работ Кодда, Дейта, Бернстайна и прочих.
Если вы не видите в этом математики, то проблема не в математике. Проблема лично в вас.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, Sinclair, Вы писали:
S>>А нельзя ли чтонть такое, что было бы практически применимо? А то всё это примеры, как программы решают проблемы программистов, созданные самими же программистами. СУБД, даже если с шедулерами и верификацией типов в налоговую инспекцию не сдашь, да и управлять ракетой тоже не поставишь.
S>Простите, но я не могу вам ничем помочь. В налоговую вы сдаёте отчёт, подписанный цифровой подписью, основанной на вполне себе конкретной математике. При подготовке этого отчёта вы пользовались СУБД, построенной на основе работ Кодда, Дейта, Бернстайна и прочих.
СУБД — это задача, которую программисты сами себе поставили (точно, сделав нужные определения сами) и сами решили.
Такая же картина наблюдается в математике — математики решили, что неплохо бы сделать цифровую подпись, выписали полный и точный список требований, решили задачу, и доказали, что решение правильно.
В реальном мире определить задачу — первая и главная трудность. Обычно невозможно точно определить явления реального мира, всякую турбулентность или действия законодателя, так, чтобы определения можно было бы практически использовать.
Соответственно, после того, как доказали, что алгоритм точно решает поставленную задачу, в случае с СУБД проблемы по определению закончились, а в случае с чем-то практически применимым через какое-то время оказывается, что реальный мир не соответствует спецификации.
DG>>насколько я помню, для не ECC-памяти — это оценивается как три случая в год при непрерывной работе устройства.
S>оценка должна зависеть от объема и физического размера памяти.
согласен.
я эту оценку встречал несколько лет назад, и тогда, на вскидку, шла речь о кол-ве памяти в районе 1-4 гб и размером с 1-2 стандартных планки dimm
ps
еще, конечно, зависит от того, как именно защищен компьютер от космического излучения (в ДЦ на глубине 1км под землей — кол-во сбоев упадет на несколько порядков)
S>СУБД — это задача, которую программисты сами себе поставили (точно, сделав нужные определения сами) и сами решили. S>Такая же картина наблюдается в математике — математики решили, что неплохо бы сделать цифровую подпись, выписали полный и точный список требований, решили задачу, и доказали, что решение правильно.
Ничего подобного. Всё наоборот — это налоговая поставила задачу "идентифицировать авторство цифрового документа", математики в ответ придумали цифровую подпись.
Из реальной жизни взялась задача складского учёта — в ответ на неё придумали реляционные СУБД и теорию транзакций.
Неважно, что этих матаппаратов недостаточно для решения вашей "задачи реального мира". Важно то, что они для вас необходимы.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, Sinclair, Вы писали:
S>Из реальной жизни взялась задача складского учёта — в ответ на неё придумали реляционные СУБД и теорию транзакций.
Разговор был вот об этом
1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель.
В случае теории транзакций,
1. Математическую модель формирует программист — какая сказано, такая и будет. Какие теоремы захотят доказать, такие докажут, а про остальные скажут "не нужно". Сами себе поставили задачу, сами и решили.
2. В теории транзакций есть полный и точный список свойств системы, поскольку систему описывали сами программисты.
3. Математическая модель есть — составить модель чего-то, что сами же и придумали, гораздо проще, чем составить модель физического склада с учетом пьянства грузчиков и воровства охраны.
Все эти примеры — оптимизирующий компилятор, реляционная СУБД, или теория транзакций, объединяет то, что нет внешнего заказчика или нет внешней проверки. Если в задании сказано "атомарность транзакций это то-то и это-то", атомарность становится тем, что сказано — "по определению". Поэтому в области программирования можно ставить себе задачи с удобными математическими моделями и "культурно" решать их. В реальном мире такое не работает. Можно, конечно, сказать "сопротивлением воздуха пренебрегаем", но воздух от этого не исчезает.
Здравствуйте, Klapaucius, Вы писали:
K>Ну, еще раз спрошу: и? Какой вывод-то? Не нужно писать "безупречные автоматы"?
Вывод такой, что на практике автоматы уже стали более безупречными, чем постановка задачи. Грубо говоря, если есть спецификация и по ней точно закодить, то через какое-то короткое время тестирования окажется, что в спецификации больше ошибок, и они дороже, чем в кодеже.
Здравствуйте, Sharowarsheg, Вы писали:
S>Если в задании сказано "атомарность транзакций это то-то и это-то", атомарность становится тем, что сказано — "по определению". Поэтому в области программирования можно ставить себе задачи с удобными математическими моделями и "культурно" решать их. В реальном мире такое не работает. Можно, конечно, сказать "сопротивлением воздуха пренебрегаем", но воздух от этого не исчезает.
Я вас продолжаю непонимать. Я вижу реальные программы складского учёта. Посмотрите, к примеру, на tpc-c. Вас беспокоит то, что там нет моделирования пьянства грузчиков?
Ну так эта задача никогда и не ставилась. Зато вот задача обеспечения целостности — ставилась. И именно для её решения были придуманы все эти шедулеры, оптимизаторы запросов, и прочая математика. А вы сейчас пытаетесь сделать вид, будто в складских программах ничего этого нет.
Ну так вот 90% складской программы работает за счёт как раз этой математики. Именно там — хардкор и основная работа. А всё, что вам кажется бессистемной программой — это тонкая плёночка, намазанная на хорошо обоснованный аппарат.
Вы можете сколько угодно говорить, что не видите роли воздуха в вашей повседневной деятельности. Тем не менее, вы им дышите.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
S>Все эти примеры — оптимизирующий компилятор, реляционная СУБД, или теория транзакций, объединяет то, что нет внешнего заказчика или нет внешней проверки.
про компилятор настолько просто, что даже ты поймешь
берем два компилятора, один не оптимизирующий, другой оптимизирующий, с кучей сложностей внутри
компилируем ими одну программу, скажем, архиватор -- получаем два бинарника (ну или экзешника, если под виндой)
запускаем на одинаковых входных данных -- получаем одинаковые результаты, но с разной скоростью
и где ты тут видишь "нет внешнего заказчика или нет внешней проверки"?
внешний заказчик -- юзер архиватора, внешняя проверка -- скорость архивации
Здравствуйте, m e, Вы писали:
ME>компилируем ими одну программу, скажем, архиватор -- получаем два бинарника (ну или экзешника, если под виндой) ME>запускаем на одинаковых входных данных -- получаем одинаковые результаты, но с разной скоростью ME>и где ты тут видишь "нет внешнего заказчика или нет внешней проверки"? ME>внешний заказчик -- юзер архиватора, внешняя проверка -- скорость архивации
2012 год. Не вижу пользователей архиватора, по большому счету.
Здравствуйте, HrorH, Вы писали:
HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?
В чрезвычайной сложности программ по сравнению с любыми другими изделиями. Программа среднего размера легко может содержать миллион запчастей, в отличии от большинства других технических изделий.
HH> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись. HH> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области) HH> 3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель, в противном случае количество вариантов будет слишком большим для такого анализа. Например, нужен анализ всех вариантов одновременных операций при доступе нескольких пользователей к иерархии ресурсов.
Если все это проделывать, то ошибки будут в вашей математической модели, в формальном описании свойств системы в полном анализе всех возможных вариантов.
Здравствуйте, Васильич, Вы писали:
В>Золотые слова. Работа программиста сравнима с работой инженера проектирующего самолет, но при этом обладает таким вреднейшим качеством, как кажущаяся легкость модификации уже сделанного.
В самолете, я думаю, меньше запчастей, чем в среднего размера программе
Здравствуйте, Sinclair, Вы писали:
S>>Так что повторюсь, вы не пожелания и мечты свои — а практику озвучьте. S>Практика перед вами ежедневно.
Т.е. в задачах, для которых есть хорошие математические модели, программисты эти математические модели активно используют. В задачах где хорошую математические модели создать не получается программисты обходятся без математики. Так в чем претензии топикстартера к программистам?
Здравствуйте, m e, Вы писали:
S>>2012 год. Не вижу пользователей архиватора, по большому счету.
ME>инсталлеры программ обычно держат программу запакованной, и распаковывают; кроме того, бывает саму программу жмут тулзой типа upx ME>тебе, как шароварщику, хоть это должно быть известно
Ну то есть как и следовало ожидать, программисты пользуются архиваторами. Распаковка обычно раз в десять быстрее, кстати сказать. И в любом случае, распаковка должна быть всего-навсего быстрее максимум десятимегабитного канала передачи, в который обычно всё упирается в дистрибутивах.
Здравствуйте, Undying, Вы писали:
U>Т.е. в задачах, для которых есть хорошие математические модели, программисты эти математические модели активно используют. В задачах где хорошую математические модели создать не получается программисты обходятся без математики. Так в чем претензии топикстартера к программистам?
Не стоит рассматривать этот топик как претензии к программистам.
Идея была в том, что человек может не совершать многие или все ошибки, если проанализирует свое мышление, и поймет, какие шаги были пропущены. Именно пропущенные шаги — это и есть наиболее частые причины ошибок.
Модель, в той или иной степени математическая (от 0 до 100%), предлагалась как одно из средств для того, чтобы найти эти пропущенные шаги.
Под математикой понимались не только различные математические области, от теории категорий до теории множеств (и меньше всего мат.анализ), но и разные виды математических и псевдо-математических нотаций, которые может придумать любой человек.
Кроме того, я считаю, что программист, который знает математику хорошо, может придумывать математические модели сам, и они будут тем более строгие математически, чем лучше он знает математику. Но строгость модели — это не самоцель.
Вообщем, если Вас смущает* слово математика, для начала считайте что его не было, так будет понятнее. A уже потом, когда станет понятно, можно степень математичности постепенно повышать от нуля и до 100%.
*смущает — здесь: вызывает протест, чувство вины, желание набить морду и другое.
Здравствуйте, Pzz, Вы писали:
Pzz>В самолете, я думаю, меньше запчастей, чем в среднего размера программе
Конечно нет. Не меньше. Поскольку в "запчасти" самолета входит несколько программ среднего размера.
Есть две причины низкой надежности софта по сравнению с самолетами:
1. Программы отличаются друг от друга сильнее чем самолеты. Возьмите конструктора самолета и поставьте ему год срока для создания автомобиля. Либо не уложится, либо автомобиль будет с багами.
2. Цена надежности. Ошибка в софте обычно обходится дешевле чем в самолете. Поэтому на искоренение багов тратится меньше ресурсов.
В принципе, писать программы на уровне самолетов вполне можно. Для космоса так и делают. Почитайте про программистов NASA, там своя специфика, но стоимость строчки кода получается абсолютно неподъемная для бизнеса ориентированного на широкого клиента.
Здравствуйте, Ziaw, Вы писали:
Z>В принципе, писать программы на уровне самолетов вполне можно. Для космоса так и делают. Почитайте про программистов NASA, там своя специфика, но
стоимость строчки кода получается абсолютно неподъемная для бизнеса ориентированного на широкого клиента.
злобный язык АДА — шаг влево, шаг вправо — расстрел через повешенье
