На сообщение:viewtopic.php?p=50114#p50114
> -- Илья Ермаков писал(а):
> Люди, вообще говоря, развиваются. Как и организации, и их проекты, и их потребности. Для меня нет "кодера", для меня есть начинающий участник работ, которому предстоит развиваться. Но начинать с основ - конкретного опыта и конкретной техники. (Признаюсь честно - врождённым "гениальностям" и эффективности "самородных талантов" я не очень доверяю - хотя бывает, что они оправдывают доверие. А вот возможности постепенного, упорного развития - доверяю. Мозгу нужна хорошая пища, которой его нужно кормить, остальное - эволюционный процесс).

Согласен, как и с большинством суждений Ильи. Вообще "кодера" можно рассматривать как рабочего в сфере производства инфопрогизделий... а снисходительное отношение к рабочим, как учит нас (м.б. не всех?) история, неоправдано... если он не может просто кодировать, а начинает изобретать - пожалуй, ему пора и правда на более высокий уровень, скорее всего после доподготовки соответствующей. Этот уровень - в традиционных терминах техника-программиста - а если нынешняя система организации данной предметки не предусматривает этого (тут и Valery Solovey говорил о том же - что делают крайности - либо "сильных", либо тупых) - то надо просто подтягивать предметку до уровня организации материального производства. Конечно, это дело сложное, но суть его ясна. Тогда смотря диалектически - если некое принципиальное противоречие инфопрогпроизводства сегодня не в этом, то в чём? Думаю, одно из противоречий просматривается опять-таки из замечательнойработы о Model Checking, если взглянуть на неё с организационно-экономической точки зрения.

Итак, в работе фактически предлагается реальный выход в практику того самого доказательного программирования, которое активно пропагандируется и на этой конференции. Какой же практический результат достижим на сегодня данным методом?
Высокая сложность ModelChecking-процесса требует его автоматизации для обеспечения широкого применения, и уже есть соответствующие среды. Автор (Ю.Г. Карпов) указывает по крайней мере одно очевидное ограничение в представлении реальных алгоритмов и программ для автоматизированной ModelChecking-верификации (на примере системы Spin и её входного импер-ЯПЗ Promela) - используются только простые типы величин, чтобы избежать текстуально неограниченной области их определения (которая обретает конечность только по результатам исполнения). Невозможно специфицировать ни типы последовательные, ни произвольные структуры с указателями, ни даже вещественно-числовые (последнее, кстати, вызывает вопрос - а что, у них не конечная, заранее фиксированная разрядная сетка мантиссы и порядка и соответственно множество возможных значений? ну да ладно м.б. здесь какая-то математическая тонкость, вроде выявленного Петровым влияния ошибок вычислений на корректность метода вычислений, сформулированного без учёта этих ошибок). Т.о. будущая программа должна оперировать этими типами величин, т.к. для них она была верифицирована (полагаем, что в конце концов успешно, т.е. контрпримеры после неоднократного их осмысления и внесения нужных изменений в спецификацию наконец перестали возникать). А если по принципиальным соображениям необходимы иные типы? Получается, тут мы пока входим в область работы ума, основанной подчас и на интуиции - изменятся ли верифицируемые свойства от введения качественно иных типов величин или нет?
Атомизация операторов - по сути дела, это их укрупнение, когда несколько действий совершаются в одном неделимом операторном ("иконном") цикле. Понятно, что в полноценной РДП-среде это делается "на раз" тем же "областным методом", о котором говорилв этом сообщении.
Видимо, следствием ограничения типов является и отсутствие файловых операций в Promela, т.к. они применимы к последовательному типу, а это опять из числа текстуально не конечных. Очевидно, надо моделировать операциями ввода-вывода в порты файловых устройств

Что же мы имеем? Получается, описание, на котором сегодня можно доказать формально и автоматизируемо правильность программы (системы программ), является упрощённым, идеализированным (чего не скрывает и Карпов). Между ним и реальным изделием, по сути, устанавливаются такие же отношения, как в материальном производстве между реальной деталью (узлом, изделием) и её чертежом. И точно так же конструктор проводит всё расчёты для идеальной модели, заданной в его документации. А при изготовлении неизбежно возникают отклонения от идеала - особенности реализации операторов на прогязыке разработки, детализация кода (снятие  ModelChecking-атомизации, которое д.б. корректным), ну и т.п. И техник, и рабочий должны не допускать брака в изготовлении. А значит, каждого из них никто не освобождает от необходимости думать, правильно ли он изготавливает - в аспекте своего уровня, разумеется. А готовят ли их именно к такой интеллектуальной деятельности? Вот здесь, по-моему, и лежит пока ещё не преодолённое противоречие. И то, что говорит Илья о постановке техники - это именно путь к его преодолению - надо только сформулировать цель приложения техник не только для инженерно-конструкторского, но и для последующих уровней данной сферы производства. Можно это показать на примере, затронутом в данной ветке:
> -- Galkov писал(а):
> В моем понимании, если у кого-то очень хорошо поставлена "техника укладки кирпичей", то это вовсе не означает, что он уже Строитель. Т.е. сможет построить Дом (надежный, имеется в виду).
> -- Илья Ермаков писал(а):
> Без техники нет выхода на более высокие уровни.
Ну, давайте поговорим о кирпичной кладке целостноДа, в практике обычный мастер-кладчик может класть, допустим, русскую печь или камин. Делает ли он это как попало? Нет, он пользуется т.н. "порядовками" - схемами кладочных слоёв, отражающими правильное с т.зр. назначения и одновременно физически реализуемое размещение кирпичей (ясно, что нельзя положить кирпич совершенно произвольно, напр. без опоры на другой в предыдущем слое). Когда-то он изучал эти схемы по чертежам или по работе мастера-учителя, постепенно освоил и кладёт автоматически, только сверяясь с источником (а часто наиболее употребительные держит в голове). При этих условиях для достижения результата ему достаточно хорошей техники укладки кирпичей во всех возможных связках (скажем, положить кирпич в текущем слое с частичной опорой на предыдущий слой нужно обычно в консольное защемление с кирпичом из слоя выше текущего).
Однако откуда взялись эти порядовки? Из результатов труда проектировщика. Согласимся, что это качественно иной труд. При этом возможно (и на самом деле изначально так и было), что результаты получались эмпирическим путём, как обобщение опыта эксплуатации печей, сложенных без первоначального проекта, интуитивно. А что было необходимо для накопления этого опыта? Дык ведь хорошая техника кладки - чтобы всё, что пришло в голову, не развалилось сразу после постройки, и можно было бы понаблюдать за его работойВот и выходит, что на качественно иной уровень, чем кладка - оптимальное проектирование выкладываемого - не выйти без освоения более низкого уровня собственно кладки... Так что классический случай когда "каждый по-своему прав"- просто Galkov выделяет одну составляющую, а Илья другую

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

И считаю правильным и для коректности мышления, и для его эффективности, экономии умственного труда, если эти техники будут иметь визуальную основу. Можно показать это на примере того же вопроса о goto - см.в этом сообщении.