DG>>можно пример когда прямой доступ поддерживает меньше операций, чем опосредованный?

K>Например, когда непосредственный доступ нарушает гарантии, которые сразу делают неработающими челый класс операций на "опосредованном" уровне.

во-первых:это значит что ты не умеешь измерять мощность операций:
1) вариантность вида — есть возможность проводить и корректные операции и некорректные операции — мощнее, чем вариантность вида — есть возможность проводить только корректные операции.
2) вариантность вида — есть возможность проводить и корректные операции, и некорректные операции + есть возможность для определенного контекста потребовать гарантию возможности только корректных операции — мощнее, чем вариантность вида — есть возможность проводить и корректные операции и некорректные операции.

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

для понимания последнего могу привести пример с истребителями последнего поколения:
1. с точки зрения планера — неустойчивое состояние — это плохо и некорректно — т.к. приводит к срыву в штопор.
2. но с точки зрения системы управления последнего поколения — неустойчивый планер — это хорошо и корректно, т.к. позволяет делать быстрые развороты, а от срыва в штопор система защищается постоянным подруливанием.

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


DG>>и что это за человек такой, который менее мощный чем посредник(язык описания)?

K>Человек в данном случае владеет мощностью языка описания, как оператор экскаватора владеет мощностью экскаватора. Ну или как оператор лопаты владеет мощностью лопаты.

DG>>во-первых: что является результатом обхода?

K>Ленивый список правильных ответов. Решатель находит первй правильный ответ, если требуем следующий — ищет дальше. Ну или не находит.

DG>>во-вторых: обход узлов гарантированно делается наиэффективнейшим образом, который ни для какого случая нельзя улучшить?

K>Не гарантировано. точно так же как и компилятор любого языка не компилирует код на этом языке в гарантированно наиэффективнейший машинный код.

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

есть неэффективное место оно должно быть заменено. точка.

K>Никто на себя таких обязательств и не берет. это невыполнимые обязательства.

берут. и именно этим обосновывается то, что инкапсуляция ничего не нарушает, и что по парето мы получаем максимум по обоим параметрам: простота, эффективность.

DG>>т.е. инкапсуляция может делаться только в обмен на гарантии: на гарантии надежности, безбажности, эффективности и т.д.

K>Не обязательно.

тогда это вредная инкапсуляция.

у тебя есть критерий — когда инкапсуляция хорошо, а когда плохо?
или для тебя всякая инкапсуляция — есть хорошо?
может тогда на разработчика вообще смирительную рубашку одеть — вообще очень хорошо все инкапсулирует.

у меня критерий есть, и он написан выше.

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

K>Для этого и надо понимать разницу между языком и реализаций. Между рантаймом и компилятором а не сваливать все в одну кучу.

это ты сваливаешь все в кучу. ты и язык уровня компиляции и runtime уровня компиляции называешь одним словом компилятор.

DG>>язык сам по себе не может добавлять операций.

K>Может.

DG>>их либо умеет делать — управляющий (человек), либо управляемый (исполнитель).

K>Уметь мало. Нужно еще и делать. Какой смысл уметь выкопать канал одной лопатой, если на практике этого не сделать?

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

K>"Емкость" и "точность" — противоречивые требования, если под точностью понимается детальность.

во-первых, есть парето-фронт — который для начала стоит достигнуть
во-вторых, парето-фронт для множества задач может состоять и из одной точки

K>Типы в разных языках выводить каким-нибудь одним констрейнт-солвером или там абстрактным интерпретатором, наверное, можно. Но это все может быть достаточно медленным по сравнению с ad-hoc реализацией для конкретного языка. Избыточная гибкость.

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

и в частности это есть следствие того, что ты не отделяешь исполнителей друг от друга, и от языка описания.

U>ps
U>Так в чем все-таки заключаются проблема вывода с помощью GridSynchronizer'а форматированного текста? Я так и не понял.

если брать virtualgridsync, то:
во-первых, он глючит
во-вторых, моргает
в-третьих, почему цвет начинает отражать наезд мышки только если строку расскоментировать?

  public partial class VirtualGridTestForm : Form
  {
    public VirtualGridTestForm()
    {
      InitializeComponent();

      var sync = new VirtualGridSynchronizer(this.panel1);
      sync.DataLink = () => new object[]
       {
         1, 2, 3, 
//         IsHover(panel1)
       };

      sync.ColumnsGetter = ()=> new IGridColumn[]
      {
        new SimpleColumn<object>("x", x=>x, new SoftTech.Gui.ColumnExtensions.CellBackColorExtension(x=> IsHover(this) ? Color.Red : Color.Green))
      };
    }

    public bool IsHover(Control control)
    {
      var position = Cursor.Position;
      var local = control.PointToClient(position);
      return 0 <= local.X && 0 <= local.Y && local.X < control.Width && local.Y < control.Height;
    }
  }

в-четвертых: как сделать чтобы внутри задания ячейки можно было использовать инфу — есть ли мышка над ячейкой, не переписывая при этом gridsync и все extension-ы?

Здравствуйте, VladD2, Вы писали:

L>>Смотри — Haskell есть и используется. OO в Haskell есть и не используется. Разницу чувствуешь?
VD>Я чувствую разницу когда вижу как используется ООЯ и как хаскель. Применение Хаскеля на фоне ООЯ не видно в микроскоп. И вижу что нет никаких проблем в совместном использовании ООП и ФП. Они прекрасно друг-друга дополняют.

Ах, как ты умеешь вовремя подменять критерии оценки! Применения Хаскеля на фоне ООЯ не видно в микроскоп, а вот совместное использование ООП и ФП оцениваем уже по твоим личным "вижу дополняют". Изумительно! Можно я тоже воспользуюсь?

Я чувствую разницу когда вижу как используется связка ФП-ООП и хаскель. Применение гибридных языков на фоне ФЯ не видно в микроскоп. И вижу что нет никаких проблем в использовании Хаскеля. Он самодостаточен.

Здравствуйте, lomeo, Вы писали:

L>>>Смотри — Haskell есть и используется. OO в Haskell есть и не используется. Разницу чувствуешь?
VD>>Я чувствую разницу когда вижу как используется ООЯ и как хаскель. Применение Хаскеля на фоне ООЯ не видно в микроскоп. И вижу что нет никаких проблем в совместном использовании ООП и ФП. Они прекрасно друг-друга дополняют.

L>Ах, как ты умеешь вовремя подменять критерии оценки!

Я ничего не подменял. Это ты начал измерять количество ОО в Хаскеле. На что тебе резонно заметили, что если уж мерить пиписьки, то по честному. Мы же не мир хаскеля обсуждаем, а вопрос совместного использования ОО и ФП. Ты утверждаешь, что это не правильно и плохо, и приводишь в доказательство "объем ОО в Хаскеле". Но это же смешно.

L>Применения Хаскеля на фоне ООЯ не видно в микроскоп, а вот совместное использование ООП и ФП оцениваем уже по твоим личным "вижу дополняют". Изумительно! Можно я тоже воспользуюсь?

Акстись. LINQ шагает по планете. Хаскелю и не снилась его популярность. Я уже не говрю про вполне успешную практику использования таких языков как Немерл, Скала и ФШарп.

L>Я чувствую разницу когда вижу как используется связка ФП-ООП и хаскель. Применение гибридных языков на фоне ФЯ не видно в микроскоп. И вижу что нет никаких проблем в использовании Хаскеля. Он самодостаточен.

Веруй в эту чушь сколько влезет. От этого ровным счетом ничего не изменит. Реалии мира таковы каковы они есть. ООП и ФП отлично уживаются в куче вполне себе живых языков (C#, VB.NET, F#, Scala, Nemerle, OCaml...).

Здравствуйте, VladD2, Вы писали:

VD>Я ничего не подменял. Это ты начал измерять количество ОО в Хаскеле.

Ну что за ерунда в самом деле? Ты уже свои фантазии мне приписываешь?
Вот эту глупость кто сказал?

А ведь если бы к в нем убрать догмы и добавить удобные для людей конструкции описания тех самых объектов мог бы получиться хороший гибрид.

VD>На что тебе резонно заметили, что если уж мерить пиписьки, то по честному. Мы же не мир хаскеля обсуждаем, а вопрос совместного использования ОО и ФП. Ты утверждаешь, что это не правильно и плохо, и приводишь в доказательство "объем ОО в Хаскеле". Но это же смешно.

Конечно смешно! Когда передёргиваешь так бывает. Потому что объём ОО в Haskell был приведён в подтверждение совсем другому тезису. А конкретно тому, что ОО в Haskell не нужен. Зачем делать отсюда далеко идущие выводы?

L>>Применения Хаскеля на фоне ООЯ не видно в микроскоп, а вот совместное использование ООП и ФП оцениваем уже по твоим личным "вижу дополняют". Изумительно! Можно я тоже воспользуюсь?
VD>Акстись. LINQ шагает по планете. Хаскелю и не снилась его популярность. Я уже не говрю про вполне успешную практику использования таких языков как Немерл, Скала и ФШарп.

Ты на что сейчас отвечал?

L>>Я чувствую разницу когда вижу как используется связка ФП-ООП и хаскель. Применение гибридных языков на фоне ФЯ не видно в микроскоп. И вижу что нет никаких проблем в использовании Хаскеля. Он самодостаточен.
VD>Веруй в эту чушь сколько влезет. От этого ровным счетом ничего не изменит. Реалии мира таковы каковы они есть. ООП и ФП отлично уживаются в куче вполне себе живых языков (C#, VB.NET, F#, Scala, Nemerle, OCaml...).

Угу! Потому что с объектами на Ocaml и F# работают столь же активно, как и на ОО-языках, я прав? А на C# и VB.NET в функциональном стиле разработка ведётся как минимум для большей части методов. Т.е. разработка на этих языках ведётся как ты описал — "абстракциях верхноего уровня — ООП, реализация — ФП + где надо ИП". Или всё таки эти слова применимы только к гибридным языкам?

Теперь конкретнее.
Применение гибридных языков на фоне ФЯ не видно в микроскоп. Гибридных языков всего-то два. На фоне огромного пласта ФЯ они действительны не видны. Только если Haskell взять, до него Scala чуть-чуть не дотягивает. А ФЯ разных чуть больше, чем один Haskell.
И вижу что нет никаких проблем в использовании Хаскеля. Ты будешь спорить с тем, что я не вижу никаких проблем с использованием Haskell?
Итак, что конкретно было чушью?

Здравствуйте, DarkGray, Вы писали:

DG>если брать virtualgridsync, то:
DG>во-первых, он глючит

В чем это заключается? У тебя версия весенняя еще? В принципе и та должна нормально работать, но лучше свежей пользоваться.

DG>во-вторых, моргает

Ему VirtualPanel надо передавать, а не обычную панель.

DG>в-третьих, почему цвет начинает отражать наезд мышки только если строку расскоментировать?

Потому что значения грида при наезде мышки на ячейку не меняются. Вызывай ForceSynchronize при наезде мыши на новую ячейку и все будет работать.

DG>в-четвертых: как сделать чтобы внутри задания ячейки можно было использовать инфу — есть ли мышка над ячейкой, не переписывая при этом gridsync и все extension-ы?

Если не меняя кода GridSynch, то отнаследоваться от него, подписаться на MouseMove и MouseLeave rowPanel и с помощью метода GetCellByClientCoord запоминать ячейку, на которой находится курсор мыши. Можно еще событие сделать, которое будет дергаться, если ячейка изменилась. Информация из грида в ячейку элементарно прокидывается через ColumnExtensionAttribute с делегатом. Если GetCellByClientCoord сделать публичным, то и наследования бы не понадобилось.

Т.е. ничего сложного, это при том, что при проектировании я о такой задачи ни разу не задумывался.

ps
Давай по этому вопрос в приват, все равно он больше никому не понятен.

Здравствуйте, DarkGray, Вы писали:

DG>сама цена зависит от того кто товар поставил, когда, по какой цене, какое отношение местной валюты к валюте поставщика и т.д.
DG>валюта цены зависит места магазины, от места покупателя, от предпочтений и возможностей покупателя и т.д.

Во-первых, в этом случае изменение будет производится точно также, только у продукта поле будет называться не Price, а BasePrice.

DG>и вот уже твоя маленькая песчинка для ответа на вопрос "сколько стоит?" должна получать на вход весь мир.

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

DG>и соответственно, ты себя обманываешь — когда считаешь, что ты понимаешь сложность задач которые [b]хочется и требуется{/b] решать.
DG>и это не идет ни в какое сравнение с той сложностью задач: которые ты уже решаешь и которую помогают решать твои текущие подходы и текущий язык.

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

U>Т.е. ничего сложного, это при том, что при проектировании я о такой задачи ни разу не задумывался.

так то, что разработчик рассмотрел задачу неполностью — это и есть основная проблема программирования.

а не рассмотреть он мог по следующим причинам:
1. вариантов слишком много и не было достаточно времени все их рассмотреть
2. код слишком большой (или слишком сложный) для обозрения и выделения всех вариантов поведения
3. забыл рассмотреть часть вариантов
4. не подумал что бывают и такие-то варианты
5. ошибся и рассмотрел варианты не верно
6. при рассматривании и фиксации в коде одно из последних вариантов косвенно внес изменения, которые изменили поведение в предыдущих рассмотренных вариантах.
7. опечатался (варианты выделены и рассмотрены верно, но при фиксации решения внесена опечатка)
8. поведение используемых частей не соответствует ожидаемому (задокументированному)

ты же эту проблему игнорируешь.

все твои замечания сводятся к:
1. достаточно написать ForceSynchronize и все будут хорошо.
2. достаточно поменять changetick и все будет хорошо.
и т.д.

но, например, замечание с ForceSynchronize сводится к следующей работе разработчика:
1. необходимо выделить все варианты работы кода, когда происходит какое-либо использование данных, которые используются при выводе gridsync-а
2. все эти варианты необходимо зафиксировать в каком-то виде (в голове, на листочке, в какой-то программе, в комментарии к коду, в коде)
3. найти время на выделение, фиксацию, разбор и внесение изменений
4. рассмотреть последовательно все варианты
5. для каждого варианта внести изменение в код: в нужное место вставить forcesynchronize
6. убедится что при внесении изменений не было опечаток
7. убедится что варианты были рассмотрены верно
8. все пункты проделать и для каждого используемого куска кода
9. после каждого изменения выполнить данные пункты заново

честная оценка трудоемкости данной работы сверху:
кол-во изменений сделанных программистом * кол-во вариантов поведения программы
кол-во вариантов поведения программы = 2^(размер всей используемой памяти (винт, heap, stack, регистры процессора и т.д.))

при данной оценке — кол-во изменений получается неважным, т.к. основной вклад дает кол-во вариантов поведения программы, и это очень огроменное число. текущие программы (например, базы данных могут оперировать и ТБ хранимых данных)
число 2^(10^12). кол-во атомов во вселенной оцениваешь лишь в 10^80 (это меньше чем 2^(10^3))

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

и gridsync по выводу данных — решает именно эту задачу, и при использовании gridsync-а достаточно рассмотреть варианты записанные в коде, и нет необходимости рассматривать все варианты изменения данных
но при вывода оформления (а не данных) через gridsync-а — данная задача не решена, и возвращает к задаче перебора всех вариантов работы кода

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

ты не понял фичу с иммутабельностью, и отвечаешь на что-то не то.
нет на самом деле в ФЯ никакой иммутабельности (с точки зрения исполнения)

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

и вот теперь объясни своими словами — как ты понимаешь данное утверждение. что программа одновременно мутабельна, и иммутабельна.

зы
ты кстати вообще понимаешь, что один и тот же код можно рассматривать с нескольких точек зрения, и записывать по разному — и при этом не меняя сам код?

т.е. представление кода меняется, а сам код не меняется.

Здравствуйте, DarkGray, Вы писали:

DG>ты не понял фичу с иммутабельностью, и отвечаешь на что-то не то.
DG>нет на самом деле в ФЯ никакой иммутабельности (с точки зрения исполнения)

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

DG>данных подход лишь утверждает, что программу мы можем одновременно рассматривать и как мутабельную, и как иммутабельную.
DG>и вот теперь объясни своими словами — как ты понимаешь данное утверждение. что программа одновременно мутабельна, и иммутабельна.

Откуда я могу знать, что ты понимаешь под данным утверждением? Разъясни, тогда я и смогу ответить как я его понял.

DG>зы
DG>ты кстати вообще понимаешь, что один и тот же код можно рассматривать с нескольких точек зрения, и записывать по разному — и при этом не меняя сам код?

DG>т.е. представление кода меняется, а сам код не меняется.

Ничего не понял. Что такое "код" и что такое "представление кода" и чем они отличаются друг от друга?

Здравствуйте, DarkGray, Вы писали:

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

Думаю, что скорее наоборот.

DG>1) вариантность вида — есть возможность проводить и корректные операции и некорректные операции — мощнее, чем вариантность вида — есть возможность проводить только корректные операции.

А что мощнее — возможность проводить корректные операции или отсутствие возможности проводить корректные операции?

DG>2) вариантность вида — есть возможность проводить и корректные операции, и некорректные операции + есть возможность для определенного контекста потребовать гарантию возможности только корректных операции — мощнее, чем вариантность вида — есть возможность проводить и корректные операции и некорректные операции.

Если второе мощнее первого, то значит вы опять со мной соглашаетесь, не соглашаясь по той же теме в предыдущем абзаце. Я дизориентирован.

DG>и это означает, что компилятор плохо, и для данного случая его необходимо заменить.

На что заменять, если все компиляторы плохие?

DG>есть неэффективное место оно должно быть заменено. точка.

Неэффективное по каким критериям?

K>>Никто на себя таких обязательств и не берет. это невыполнимые обязательства.
DG>берут. и именно этим обосновывается то, что инкапсуляция ничего не нарушает, и что по парето мы получаем максимум по обоим параметрам: простота, эффективность.

Ну приведите пример: язык, разработчик, "сокрытие возможности доступа", обоснование.

DG>>>т.е. инкапсуляция может делаться только в обмен на гарантии: на гарантии надежности, безбажности, эффективности и т.д.
K>>Не обязательно.
DG>тогда это вредная инкапсуляция.

Для кого вредная? Если разработчик что-то инкапсулирует — это развязывает ему руки, позволяя что-то менять за "стенами" инкапсуляции и это облегчает для него соблюдения каких-то инвариантов.

DG>у тебя есть критерий — когда инкапсуляция хорошо, а когда плохо?

Есть. И не один.

DG>или для тебя всякая инкапсуляция — есть хорошо?

Нет.

DG>может тогда на разработчика вообще смирительную рубашку одеть — вообще очень хорошо все инкапсулирует.

Зависит от обстоятельств. Если разработчик психопат — это может быть полезным, наверное.

DG>у меня критерий есть, и он написан выше.

Там нет критерия — там отрицательная эвристика. Вы не пишете, когда инкапсуляция это хорошо, но пишете, когда инкапсуляция это плохо — когда нельзя дать перечисленных гарантий. Гарантии эти дать нельзя — следовательно инкапсуляция это всегда плохо и всегда не нужна. Так получается?

DG>это ты сваливаешь все в кучу. ты и язык уровня компиляции и runtime уровня компиляции называешь одним словом компилятор.

Что означают словосочетания "язык уровня компиляции" и "runtime уровня компиляции"?

K>>Уметь мало. Нужно еще и делать. Какой смысл уметь выкопать канал одной лопатой, если на практике этого не сделать?
DG>так для этого и нужны исполнители.
DG>один умеет копать — фиксирует это умение с помощью языка описания — и передает тем кто может махать лопатой (или может двигать произвольным предметом, или еще что-нибудь), а они уже копают.

Какой смысл уметь фиксировать A с помощью языка B, если на практике этого не сделать?

K>>"Емкость" и "точность" — противоречивые требования, если под точностью понимается детальность.
DG>во-первых, есть парето-фронт — который для начала стоит достигнуть
DG>во-вторых, парето-фронт для множества задач может состоять и из одной точки

Туманные фразы никогда не становятся точкой на графике. Для того, чтобы получать точки нужно что-то более формализованное.

K>>Типы в разных языках выводить каким-нибудь одним констрейнт-солвером или там абстрактным интерпретатором, наверное, можно. Но это все может быть достаточно медленным по сравнению с ad-hoc реализацией для конкретного языка. Избыточная гибкость.
DG>и это означает, что ты рассматриваешь как догму, что универсальный модуль не может быть эффективным для частной задачи (что он не умеет перестраиваться так, что будет максимально эффективным на частной задаче).
DG>и в частности это есть следствие того, что ты не отделяешь исполнителей друг от друга, и от языка описания.

Ну, догматизм из слов "наверное можно" и "может быть" я тоже не способен выводить. Мои возможности вообще довольно ограничены.

Здравствуйте, DarkGray, Вы писали:

DG>но, например, замечание с ForceSynchronize сводится к следующей работе разработчика:

Какой-то жуткий формализм, который непонятно как применять на практике.

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

Но допустим, что такая задача появилась, далее качество решения можно оценить с двух позиций:
1) Насколько просто решить эту задачу не меняя код решения.
2) Насколько просто решить эту задачу изменяя код решения.

Как эта задача решается первым способом я тебе уже показал. Из косяков там только необходимость наследования, возникшая из-за того, что так как грид я писал под себя, то не задумывался какие методы имеет смысл делать публичными, а какие нет, т.к. легко могу увеличить область видимости, когда потребуется. А также необходимость вызова ForceSynchronize, это да проблема решения.

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

Что тебе еще надо от решения?

U>samius под иммутабельностью понимал наличие в программе только иммутабельных объектов, из чего следует что внесение изменений в мир производится через создание нового экземпляра мира. Именно про эту иммутабельность я и веду речь. Если ты о какой-то другой иммутабельности, то расскажи о какой.

это способ представления кода.
компилятором на основе этого иммутабельного представления генерятся мутабельные объекты и мутабельный код.
так понятнее?


DG>>данных подход лишь утверждает, что программу мы можем одновременно рассматривать и как мутабельную, и как иммутабельную.
DG>>и вот теперь объясни своими словами — как ты понимаешь данное утверждение. что программа одновременно мутабельна, и иммутабельна.

U>Откуда я могу знать, что ты понимаешь под данным утверждением? Разъясни, тогда я и смогу ответить как я его понял.

DG>>зы
DG>>ты кстати вообще понимаешь, что один и тот же код можно рассматривать с нескольких точек зрения, и записывать по разному — и при этом не меняя сам код?

DG>>т.е. представление кода меняется, а сам код не меняется.

U>Ничего не понял. Что такое "код" и что такое "представление кода" и чем они отличаются друг от друга?

код — это запись последовательности исполнения с помощью определенных правил.
например, выражение a + b *c можно записать как (и это будут разные представления одного и того же кода):

1. a + b * c
2. a+b*c
3. a + (b * c)
4. add(a, mul(b,c))
5. + (a (*(b c))) // префиксная, она же польская запись
6. new[]{a, new[]{b, c}.mul()}.add()
7. (a (b c)mul)add
8. (a (b c)*)+ //постфиксная запись
9. a1 + a2 * a3
10. a[1] + a[2] * a[3]
11. a.x + b.x * c.x
12. x.a + x.b + x.c

и есть правила(алгоритмы) — которые позволяют одно представление преобразовать в другое представление (при этом гарантируя, что исполнение при этом не поменяется)
далее фиксируется отличие. и правила преобразования отличия
1 <-> 2. пробельные символы есть/нет. преобразование 1->2 заменить все пробелы на пусто, 2->1 вокруг знаков операций расставить по одному пробелу
1 <-> 3. 1->3 расставить скобки, которые показывают какой будет действительный порядок выполнения, 3->1 убрать скобки, которые следует из приоритетов операций
3 <-> 4. запись делается или через операции, или через функции. 3->4 каждую тройку operand op operand заменить на function(op) (operand operand)
4->3 каждую тройку function (operand operand) заменить на (operand function.op operand)
//далее правила преобразования не фиксирую, связи с экономией времени
3<->5. операция записывается до операндов или между
3<->8. операция записывается после операндов или между
3<->9. имена переменных другие
3<->10. переменные рассматриваются как хранящиеся в массиве
3<->11. переменные рассматриваются как запакованные в какой-то другой тип
3<->12. переменные рассматриваются, как часть другой структуры

зачем все это надо?
если по коду надо ответить на какой-то вопрос (решить задачу над кодом), то часто по одному из представлению задачу решить намного проще, чем по другому.

задача:
1. понять(обозреть) что вообще делается — проще решается по первому 1.
2. получить минимальный листинг, который будет еще понятен компилятору — представление 2
3. зафиксировать в каком порядке точно будут выполняться операции — представление 3
4. какие функции будут вызываться и в каком порядке? представление 4
5. если исполнитель стековая машина, то в каком порядке числа будут помещаться на стек и обрабатываться? представление 8
6. какой длины массив необходим для хранения исходных данных для выражения? представление 10
7. как выражение будет выглядеть для nullable-типа, при отсутствии перегруженных операций? представление 11
8. какую структуру необходимо сделать, чтобы хранить исходные данные выражения? представление 12.


2. можно зайти с другой стороны.
рефлектором когда-нибудь пользовался?
обращал внимание на то, что он по одному и тому же IL-у может сгенерить листинги на IL, C#, VB, Delphi, MC++, Oxygene, F#? так же еще можно и выбрать версию языка. допустим для .net-а можно выбрать 1.0, 2.0, 3.5 и 4.0
и соответственно получается, что код-то один (он в dll-ке зафиксирован, а представить мы его можно на разных языках)

3. или взять тот же var
явная(тип указан явно) запись и неявная(указывается var) эквиваленты, и это два разных представления одного и того же кода
1. у первой записи преимущества, что она позволяет явно зафиксировать тип результата, и не допускает вольных трактовок
2. вторая запись позволяет не фиксировать тип результата

для простого кода оба преимущества не критичны

var x = 1 + 4;
int x = 1 + 4;

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

//одно дело записать var, другое дело - руками явно записать тип результата
var index = this.GetType().Properties().GroupBy(property=>property.Name).ToDictionary(group=>group.Key, group=>group.ToArray());

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

вот только ты почему это допущение забыл упомянуть — когда я говорил — что есть проблема с отрисовкой оформления ячеек при gridsync, а ты меня убеждал в обратном.

U> Какой-то жуткий формализм, который непонятно как применять на практике.

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

> который непонятно как применять на практике.

для этого достаточно открыть умную книжку, или меня спросить

U>Что тебе еще надо от решения?

гарантий, что код всегда работает, работает правильно, работает правильно и максимально эффективно.

вот представь, что тебе надо допустим отправить херотень на луну. предположим, что технических проблем нет, надо только правильно все закодировать.
задача очень сложная, у тебя в подчинении 200-программистов — которые колбасят какой-то код, и каждый зуб дает, что его код уж точно не содержит ошибок.
попытка у тебя только одна, за неудачу надо отвечать лично перед товарищем Берией, который знает только одно — что если хренотень сделала что-то неправильно, то значит ты лично допустил разгильдяйство и подлежишь расстрелу.
также пока предположим, что ресурсов у тебя бесконечно для решения данной задачи.
твои действия? как тебе минимизировать неудачу и свой расстрел?

K>А что мощнее — возможность проводить корректные операции или отсутствие возможности проводить корректные операции?

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

DG>>2) вариантность вида — есть возможность проводить и корректные операции, и некорректные операции + есть возможность для определенного контекста потребовать гарантию возможности только корректных операции — мощнее, чем вариантность вида — есть возможность проводить и корректные операции и некорректные операции.

K>Если второе мощнее первого, то значит вы опять со мной соглашаетесь, не соглашаясь по той же теме в предыдущем абзаце. Я дизориентирован.

чего? что такое "второе мощнее первого"?

DG>>и это означает, что компилятор плохо, и для данного случая его необходимо заменить.

K>На что заменять, если все компиляторы плохие?

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

DG>>есть неэффективное место оно должно быть заменено. точка.

K>Неэффективное по каким критериям?

по всем с точностью до парето-фронта

K>Ну приведите пример: язык, разработчик, "сокрытие возможности доступа", обоснование.

1. assembler->маш.код, разработчик каждого ассемблера, отсутствие возможности влиять на трансляцию, преобразование эквивалентное и там нечего менять.
2. почти все языки,, сокрытие возможности менять встроенные типы, они один в один ложатся на регистры процессора и с точки зрения эффективности выполнения менять по большому счету нечего.

DG>>тогда это вредная инкапсуляция.

K>Для кого вредная? Если разработчик что-то инкапсулирует — это развязывает ему руки, позволяя что-то менять за "стенами" инкапсуляции и это облегчает для него соблюдения каких-то инвариантов.

для определенного круга пользователей (и кстати отсутствием лишних инкапсуляций обосновывается преимущество open-source над closed-source).

т.е. разработчик не уверен, что его решение после выпуска идеальное, и хочет его менять параллельно с тем, как другие его используют?
а если оно идеальное, то зачем он его хочет переписывать?


K>Там нет критерия — там отрицательная эвристика. Вы не пишете, когда инкапсуляция это хорошо, но пишете, когда инкапсуляция это плохо — когда нельзя дать перечисленных гарантий. Гарантии эти дать нельзя — следовательно инкапсуляция это всегда плохо и всегда не нужна. Так получается?

введение инкапсуляции всегда ухудшает параметр гибкость.
поэтому да с точки зрения гибкости инкапсуляция это всегда плохо.

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

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

и например, для open-source можно считать, что как раз предоставляется не жесткая инкапсуляция, т.к. можно в любое время исходник переписать под себя. но тут мы приходим к параметру качества исходника с точки зрения его меняемости, а также стоимости сопровождения fork-а

DG>>это ты сваливаешь все в кучу. ты и язык уровня компиляции и runtime уровня компиляции называешь одним словом компилятор.

K>Что означают словосочетания "язык уровня компиляции" и "runtime уровня компиляции"?

язык уровня компиляции — понятия которого существуют только на уровне компиляции, и не существуют при выполнении.
runtime уровня компиляции — исполняемый код, который работает только на уровне компиляции, и отсутствует на этапе выполнения.

простейшим примером первого и второго является допустим язык макросов в C и макро-процессор в C
более сложным примером является исполняемый код, который выводит тип результата. языком для этого исполнителя(runtime-а) — будет система значков, которая упрощает вывод типа результата.


K>>>Уметь мало. Нужно еще и делать. Какой смысл уметь выкопать канал одной лопатой, если на практике этого не сделать?
DG>>так для этого и нужны исполнители.
DG>>один умеет копать — фиксирует это умение с помощью языка описания — и передает тем кто может махать лопатой (или может двигать произвольным предметом, или еще что-нибудь), а они уже копают.

K>Какой смысл уметь фиксировать A с помощью языка B, если на практике этого не сделать?

чего? что такое "А"?
а вообще это фиксируется сплошь и рядом.

Здравствуйте, DarkGray, Вы писали:

DG>вот только ты почему это допущение забыл упомянуть — когда я говорил — что есть проблема с отрисовкой оформления ячеек при gridsync, а ты меня убеждал в обратном.

Изначально ты говорил о следующих проблемах:

1. вывод в ячейке что-то отличного от просто текста (раскраска, форматирование, вывод rich-текста и т.д.)
2. поддержка rowspan, colspan-ов
3. вывод нескольких разнородных источников на одну сетку грида

Затем ты понял, что все перечисленное не является проблемой, и перескочил на другую тему.

Проблема у подхода с кэшами на самом деле есть, но она совсем в другом. Кэши отлично отвечают на вопрос, что нужно сделать, чтобы получить правильное состояние программы, но кэши не могут ответить на вопрос — когда нужно это сделать. Соответственно в gridSynchronizer'е, как частном случае подхода с кэшами, это проблема тоже есть. И решается она через периодическое принудительное сравнение текущего состояния входа кэша с запомненным. Однако такой подход имеет очень существенный недостаток, а именно медлительность. Большая частота синхронизации чревата тормозами, а при синхронизации 1-2 раза в секунду задержка при обновлении заметна пользователю. Соответственно избавиться от ручной синхронизации не получается, после выполнения действий приходится вызывать ForceSynchronize. Однако подход с кэшами позволяет нам обновление производить простым и однообразным образом (ForceSynchronize тяжело вызвать неправильно), а подход с периодической синхронизацией гарантирует, что, даже если мы забудем в каком-то случае явно вызывать обновление, приложение все равно будет работать корректно, хоть и не идеально.

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

DG>гарантий, что код всегда работает, работает правильно, работает правильно и максимально эффективно.

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

DG>вот представь, что тебе надо допустим отправить херотень на луну. предположим, что технических проблем нет, надо только правильно все закодировать.
DG>задача очень сложная, у тебя в подчинении 200-программистов — которые колбасят какой-то код, и каждый зуб дает, что его код уж точно не содержит ошибок.
DG>попытка у тебя только одна, за неудачу надо отвечать лично перед товарищем Берией, который знает только одно — что если хренотень сделала что-то неправильно, то значит ты лично допустил разгильдяйство и подлежишь расстрелу.

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

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

Важность задачи кардинально поменяет лишь административную часть. А именно функции и тесты должны писаться в нескольких вариантах, людьми никак не связанными друг с другом, выполнение действий должно резервироваться, отдельные модули должны испытываться на реальных, но менее важных и дорогостоящих задачах.

U>Ты хоть одно решение, дающее такую гарантию, можешь показать? А то я еще не встречал ни одного человека, который был бы не согласен с тем, что хорошо быть и богатым, и здоровым. Проблема только в том, что непонятно как сие желание преобразовать в решение.

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

Можно выделить два направления: условно назовем их "языкостроение" и "платформостроение".
"Языкостроение" — направлено на развитие языков, которые обеспечивают доказательство правильности работы программ
"Платформостроение" — направлено на развитие платформ, уменьшаюших степень фатальности ошибки. Развитие идет через выделение подмножества средств, которые с одной стороны — дают гарантию, что их использование не может привести к фатальным ошибкам, а с другой стороны — достаточны мощны для решения данных классов задач

По первому направлению сильного продвижения нет, и пока оно больше остается нишевым, из которого идет перекачка в mainstream.
примером такой перекачки является, например, статическая типизация, которая усиливается от версии mainstream-языков к версии (например, в .net-4 в статическую типизацию добавили понятия covariance и contravariance, до этого в 3.5 добавился вывод типов)

Второе направление "платформостроение" получило большее распространие в mainstream-е, чем языкостроение, появились такие платформы как:
1. браузер/javascript — из языка убраны управление потоками и прямой доступ к памяти.
2. sql-движок/sql,xpath,xquery — из языка убраны циклы, убраны прямой доступ к памяти, управление потоками
3. .net, java/C#,java,vb.net — из языка поумолчанию(можно включить) убран прямой доступ к памяти, через CAS можно убрать управление потоками
4. Plc-платформа/языки IEC 61131-3 — из языка убран прямой доступ к памяти, убраны циклы (цикличность делается через глобальный цикл всей платформы)
и т.д.

именно эти средства убираются по следующим причинам:
1. прямой доступ к памяти убирается, потому что при его отсутствии каждый кусок кода имеет доступ только к данным, ссылки на которые ему явно переданы. это дает гарантию локальности ошибки.
2. убирание циклов — позволяет получить гарантию, что программа закончится за конечное время
3. убирание управления потоков — усиливает первую гарантию (два потока могут иметь несинхронизованный доступ к общей памяти и получить в том числе невалидные указатели, которые предоставят доступ к чужим данным), и усиливают гарантию законченности (два потока могут повиснуть на deadlock-ах)

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

забываешь самое главное: первая главная задача программиста доказать что обработаны все варианты поведения.
то, что ты зафиксировал — это лишь способ уменьшения кол-ва вариантов поведения программы, и этот способ лишь упрощает выполнение главной задачи.

даже тестирование программы опирается именно на эту задачу: задача тестирования покрыть тестами все варианты поведения программы.
если варианты покрыты не полностью значит тестировщики не выполнили свою задачу.

для следующего примера не надо никаких тестов, в нем уже при простейшей статической проверки видно, что не обработан вариант с null-ом

void Q(string s)
{
   if (s.ToLower() == "a")
     ...
}

здесь видно что не обработан вариант, когда items — null и когда 5 находится на первом месте в массиве

void Q(int[] items)
{
  for (int i = 0; i < items.Length; ++i)
  {
    if (items[i] == 5 && items[i-1] == 4)
     ...
  }
}

и т.д.

U>Важность задачи кардинально поменяет лишь административную часть. А именно функции и тесты должны писаться в нескольких вариантах, людьми никак не связанными друг с другом, выполнение действий должно резервироваться, отдельные модули должны испытываться на реальных, но менее важных и дорогостоящих задачах.

и это подтверждает, что ты далек от программирования, которое занимается решением сложных и критических задач.

то, что ты написал — не дает никакой гарантии, и это подтверждает взрыв Ариана 5 — там использовалось ПО, которое уже даже успешно отработало на Ариан 4.
http://www.ci.ru/inform11_97/vzrv.htm
и что самое интересное, что при разборе причин аварии, было выяснено, что
1. во-первых, разработчики поленились в паре мест с доказательством гарантии работоспособности программы
вернее для обоснования доказательства использовался довод, что такого не бывает (таких высоких величин не бывает)

Комиссии сообщили, что не все преобразования были защищены, потому что для компьютера SRI была установлена максимальная рабочая нагрузка в 80%. Чтобы определить уязвимость незащищенного кода, при разработке выполнялся анализ для каждой операции, которая могла бы вызывать исключительное состояние, включая ошибку операнда. В частности, было проанализировано преобразование чисел с плавающей запятой в целые числа, и найдены семь переменных, действия с которыми могли привести к ошибкам операнда. В результате этого была добавлена защита для четырех переменных. Однако три переменные были оставлены незащищенными. Никаких прямых ссылок на оправдание этого решения не было найдена в исходном коде.

Три остающихся переменных, включая ту, что обозначала горизонтальное смещение, были не защищены. Это было сделано на основе рассуждений, которые показывали, что значения этих переменных были физически ограничены или имелся большой запас по безопасности — рассуждения, которые для переменной BH оказались ошибочными.

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

Хотя источник ошибки операнда был идентифицирован, само по себе это исключительное состояние не приводило к отказу. Отказу способствовала и специфика механизма обработки особых ситуаций: в случае любого вида исключительной ситуации, согласно спецификации системы, сбой должен быть отражен на шине данных, состояние системы на момент сбоя должно быть сохранено в памяти ЭСППЗУ (которое было найдено и прочитано в случае с Ariane 5) и, в заключение, процессор SRI должен быть остановлен.

кстати вывод коммиссии подтверждает мои слова о том, что программу надо доказывать

Исключительная ситуация была обнаружена, но была обработана неподобающим образом, потому что было принято считать, что ПО должно рассматриваться, как правильное, пока не доказано обратное. Комиссия имеет основания предполагать, что этот же принцип лежит в основе и других разработок ПО для Ariane 5. Комиссия придерживается противоположной точки зрения — что ПО должно изначально считаться содержащим ошибки, пока использование принятых в настоящее время самых лучших практических методов не докажет, что оно правильное.

U> добавить в gridSynchronizer входы не связанные с ячейками дело пятнадцати минут.

любая локальная проблема решается за "15 минут", но это не дает гарантию, что:
1. после внесения изменений не возникло несколько других проблем в других местах
2. все такие проблемы могут быть решены за конечное реальное время
3. проблема будет решена до того, как она станет критичной (проблема проявилась на реальном важном пуске, нет в наличии "15 минут", нет технической возможности внести исправление)

Здравствуйте, DarkGray, Вы писали:

DG>он один: доказать полностью, что программа правильно работает.

И каким образом можно доказать правильно работы не то что программы, а хотя бы одной, но достаточно сложной функции? Ту же функцию контроля расписания я тебе приводил, объясни как можно доказать ее правильность?

DG>"Платформостроение" — направлено на развитие платформ, уменьшаюших степень фатальности ошибки. Развитие идет через выделение подмножества средств, которые с одной стороны — дают гарантию, что их использование не может привести к фатальным ошибкам, а с другой стороны — достаточны мощны для решения данных классов задач

С этим согласен. И это правильный путь, в отличие от мифического доказательства правильности программ.

DG>забываешь самое главное: первая главная задача программиста доказать что обработаны все варианты поведения.
DG>то, что ты зафиксировал — это лишь способ уменьшения кол-ва вариантов поведения программы, и этот способ лишь упрощает выполнение главной задачи.

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

DG>[/q]
DG>2. во-вторых, платформа исполнения при локальном сбое останавливало всю систему (вместо локализации ошибки, и остановки только части исполняемого кода)
DG>

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

DG>кстати вывод коммиссии подтверждает мои слова о том, что программу надо доказывать
DG>[q]
DG>Исключительная ситуация была обнаружена, но была обработана неподобающим образом, потому что было принято считать, что ПО должно рассматриваться, как правильное, пока не доказано обратное. Комиссия имеет основания предполагать, что этот же принцип лежит в основе и других разработок ПО для Ariane 5. Комиссия придерживается противоположной точки зрения — что ПО должно изначально считаться содержащим ошибки, пока использование принятых в настоящее время самых лучших практических методов не докажет, что оно правильное.

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

U>Вывод комиссии неверен, т.к. является классическим пожеланием благих намерений, которые невозможно применить на практике. Правильный вывод такой — "ПО должно изначально считаться содержащим ошибки, поэтому должно гарантироваться, что любая одиночная непредвиденная ошибка не должна приводить к выходу программы из строя". Из этого следует, что резервироваться должна не только аппаратика, но и программый код, т.к. вероятность того, что решение задачи написанное независимо разными людьми содержит одинаковые ошибки много ниже вероятности наличия в этих же решениях разных ошибок.

верен. ты, кстати, используешь довод — я не умею доказывать программы, поэтому это никто не умеет.

другие разработки, например, ПО для самолета C-130 делается на языке Spark (это расширение Ada-ы со статическим контролем pre/post-условий)

http://www.altran-praxis.com/spark.aspx
http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/lesson_contracts/

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

теми же способами которыми доказываются теоремы. а теорема того же ферма намного сложнее чем большинство программ.
теоремы в универе доказывал? алгоритм доказательства помнишь?

берутся аксиомы, с помощью выводов доказываются более сложные следствия и вперед по накатанной.
тоже самое и с программой.

базовые операции a+b, if, for и т.д. считаются верными на фиксированном классе значений, а дальше вперед:
для каждого куска кода фиксируется pre/post-условия, инвариант.

> Ту же функцию контроля расписания я тебе приводил, объясни как можно доказать ее правильность?

в том виде — в котором оно записано — тяжело.
если переписать в ФЯ-шный вид, намного проще.
если записать ее через сведение к стандартным алгоритмам — сортировка, поиск, поиск путей в графе, динамическое программирование и т.д. то еще проще.
твою задачу можно свести к чему-то между топологической сортировкой и поиском пути в графе.
можно также доказать ее через динамическое программирование.

при использовании динамического программирования — доказательство элементарное.
динамическое программирование исходит из того, что:
1. на каждом шаге уже есть какое-то частичное хорошее решение,
2. каждый следующий шаг улучшает это решение на 1/n
3. итого, через n-шагов будет полное решение.
доказать лишь надо, что на каждом этапе существует шаг, который улучшит результат как минимум на 1/n.

этим способом, например, легко доказать верность алгоритма сортировки прямого выбора.

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

ты это расскажи математикам — что ничего доказать нельзя.
99.9% задач которые ты решаешь — имеют готовые доказанные алгоритмы, и это еще было сделано лет 100 назад.

ты хоть чуть-чуть теорию программирование ботал? не практику, а именно теорию.
хотя бы кнута, таха и т.д. — а у них там сплошные доказательства правильности работы алгоритма.