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

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

HH>при разработке теории функционального реактивного программирования этому Conal Elliot в голову пришла идея.
HH>Во-первых, надо говорить про денотационную семантику (это то что придумали в 1960)
HH>and Dana Scott in the 1960s (Scott and Strachey 1971; Stoy 1977).
Да-да, очень свежие идеи.
И конечно чистая случайность что они не выстрелили до сих пор

HH>Так, вот тут есть семантическая функция, которая сопоставляет синтаксису в коде его значения в модели.
Погуглил "рядом" с указанными источниками. Многовато речи идет о DSL. Вы уверены что DSL это "математика"?

HH>Так вот, идея была в том, что могут быть законы, которые выполняются для этой семантической функции.

HH>Вот обсуждение этого в блоге Вадлера
HH>Кстати он там рекомендует посмотреть

HH>Вот эти 2 бумаги кажется основные.
И посвящены языковым проблемам, а не проектированию и верификации ПО.

Посмотрел также CV Conal Elliott, потому что вобщем-то у вас он единственный свежий источник вдохновения.
То что сейчас он хаскелист ладно.
Смотрим что же привело его к этому, какая такая трудовая биография.
А там — сплошь графические алгоритмы, 2D, анимайтед 3D, вертексы с шейдерами из C# и проч.
То есть сама область — сугубая математика. То есть человек вырос на чисто математических задачах
Далее, вырос так что и начал заниматься "DSL" — Vertigo, a language and compiler for computations on graphics processors.
или: Pajama a compiler to produce highly optimized Java applets from simple, declarative specifications of interactive media (e.g., imagery, animation, sound).

HH>Но меня поразило именно то, что все эти апликативные функторы, монады и т.д. использовались именно для определения семантики программы, а сама реализация по мере развития библиотеки делалась более эффективной, то есть использовались другие конкретные типы, но сама модель оставалась почти неизменной.
А чего моделям с которыми работал Conal Elliott изменяться?
Такая у него предметная область — устойчивая.

HH>В конце концов Вадлер на ерунду обращать внимание не стал бы
Хорошо, читаем кто такой этот Вадлер:
Philip Wadler
Position: Professor
Roles: Member of Laboratory for Foundations of Computer Science
Research Interests: Programming languages, functional programming, type systems, web programming, query languages for databases, hybrid and gradual typing, Haskell, Erlang, Java, XML.

То есть "академик" и преподаватель, как понимаю с его емайла inf.ed.ac.uk.
Cугубо научная работа. С чистенькими, рафинированными проблемами.

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

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

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

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

M>покажи пример кода при геттерном подходе

http://rsdn.static.corbina.ru/forum/design/3612218.1.aspx

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

ты опять про внутренние объекты, а я тебе про внешние объекты: БД, файловая система, UI, сеть и т.д., и взаимодействие с ними.

например, если есть набор объектов Button, то чтобы задействовать все поля Button-а через getter-ы необходимо добавить внутренний объект ButtonState + добавить class ButtonSynchronizer, который применяет ButtonState к Button.

U>Падает, но это одно из следствий. А нас интересует причина почему это происходит.

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

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

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

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

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

DG>ты опять про внутренние объекты, а я тебе про внешние объекты: БД, файловая система, UI, сеть и т.д., и взаимодействие с ними.

Там все то же самое только вместо автоматических кэшей используются LazyMaker'ы.

DG>например, если есть набор объектов Button, то чтобы задействовать все поля Button-а через getter-ы необходимо добавить внутренний объект ButtonState + добавить class ButtonSynchronizer, который применяет ButtonState к Button.

Зачем? Пишется LazyMaker зависящий от нужных входов, вызов LazyMaker.Make вставляется в OnPaint контрола, если входы изменились, то вызывается обработчик, изменяющий нужные свойства Button'а. Соответственно если какие-то изменения нам нужно немедленно отобразить пользователю, то достаточно после выполнения изменений выполнить перерисовку формы. Код UI становится примитивней паровоза, никакого сравнения с событийным кошмаром.

U>Зачем? Пишется LazyMaker зависящий от нужных входов, вызов LazyMaker.Make вставляется в OnPaint контрола, если входы изменились, то вызывается обработчик, изменяющий нужные свойства Button'а.

Т.е. никакой инкапсуляции? это возможно только для каких-то очень простых программ с отношениями только вида 1 к 1.
возьмем, например, графический редактор схем, состоящий из нескольких widget-ов: поле и список всех элементов.
допустим, что элементы подписываются и на поле, и в списке.
как тогда запишется правило, что название выделенного элемента должен выводится жирным зеленым шрифтом с размером на 10% больше умолчательного?

зы
в первом приближении, чтобы не было дублирования — это записывается или так (это будет Push):

void UpdateControl_ForSelectedElement(Control control)
{
  control.Font = new Font{Bold=true, Size = default.Font.Size * 1.1};
  control.Color = Colors.Green;
}

или так (pull):

ControlState ControlState_ForSelectedElement()
{
  return new ControlState
  {
    Font = new Font{Bold=true, Size = default.Font.Size * 1.1};
    Color = Colors.Green;
  };
}

или так (pull, в идеале):

ControlState ControlState_ForSelectedElement()
{
  return new ControlState
  {
    Font = new FontState{Bold=true, SizeK = 1.1};
    Color = Colors.Green;
  };
}

соответственно, и появляется <T>State и <T>Synchronizer для каждого внешнего class-а <T>

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

U>>Зачем? Пишется LazyMaker зависящий от нужных входов, вызов LazyMaker.Make вставляется в OnPaint контрола, если входы изменились, то вызывается обработчик, изменяющий нужные свойства Button'а.

DG>Т.е. никакой инкапсуляции?

Причем здесь инкапсуляция и какие с ней могут быть проблемы?

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

LazyMaker selectedElementMaker = new LazyMaker(delegate
  {
    selectedElement.Control.Font = new Font{Bold=true, Size = default.Font.Size * 1.1};
    selectedElement.Control.Color = Colors.Green;
  },
  delegate { return selectedElement; }
);

void OnPaint()
{
  selectedElementMaker.Make();
}

DG>соответственно, и появляется <T>State и <T>Synchronizer для каждого внешнего class-а <T>

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

U> Причем здесь инкапсуляция и какие с ней могут быть проблемы?

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

U> LazyMaker selectedElementMaker

тогда уж (если все-таки хочется инкапсуляцию)

LazyMaker selectedElementMaker = new LazyMaker(()=>UpdateControl_ForSelectedElement(selectedElement.Control),
 delegate { return selectedElement; }
);

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

зы
фактически LazyMaker использует промежуточный подход:
push заменен на pull для отслеживания зависимостей между элементами, но сами данные push-атся

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

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

Точные замечания.

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

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

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

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

И какой же выход предлагают адепты ФП, хаскелей и "математики"?
На самом то деле ничего радикального. они предлагают то же самое что уже и так есть:
добиться восстановления модели из символьной записи, чтобы протестировать эту модель автоматизированными средствами.
Но восстановления — КЕМ? Человеком? А чем математическая запись проще в чтении чем код на ЯП? Например: Сколько времени понадобилось проверять доказательство Григория Перельмана? Или — почему Степанов на лекции в Яндексе говорил что наука построена на доверии, "у меня просто нет времени проверить даже 20ти страничное доказательство которое мне друг месяц тому дал почитать"

А если НЕ человеком, то хоть битами записывай 0110111001 — компьютер не устает и не ошибается при чтении.

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

Что же до "доказательства верности программ", то я вообще слабо представляю, как математики, которые не решили проблемы, автоматического доказательства утверждений у себя, собираются помочь в этом программистам?
Где та методика у самих математиков — наваял Перельман доказательство — запихнули его в компьютер, или просто по листикам раздали студентам с "инструкцией выполнения" и опа — "доказательство верно!" или "доказательство неверно в такой строчке на такой-то странице!"

S>Более обобщенно — какая "алфавитно"-символьная запись позволяет бороться с таким рассогласованием, и наоборот — позволяет быстро восстановить модель в уме человека?

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

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

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.
HH> 1) Не формулируется математическая модель...

Всё ясно. Как уже правильно обобщил Carc, математик пытается умничать в области, где сам ниструя не понимает.
Программинг только на заре 70-ых был "академическим", да и то математика там привлекалась только в силу требуемых алгоритмов. В целом же, программинг — это вообще отдельная дисциплина, где не то что "математическую модель", пару квадратов на бумаге — и то сложно расположить! Простой пример: GUI usability. Психология+интуиция+чтобы работало. Или вот базы данных — их что, по рядам Фурье считают? Далеко нет. Тупо "на практике" проверяют, будет ли отзывчивой система при 20 запросах в сек. Почему 20? Да просто эмпирика!
Кроме того, сидеть и рисовать мат.абстракции — это и студент в туалете может, ты попробуй напиши то, чего ещё НИКОГДА НЕ БЫЛО! Ну типа как придумать свою теорему Ферма. Этим и занимаются настоящие профи — на базе опыта, статей, чутья, каких-то полуабстрактных моделей пытаются хотя бы набросать каркас будущей системы. Тут не математика, тут даже бубен сто крат полезнее!
А говносистемы получаются не от зла большого — просто не у всех есть нужный опыт и инженерное мышление. Но пробовать-то надо! Глядишь — вторая система будет намного лучше. Кстати, "говносистемы" как раз и получаются из-за того, что один говноархитектор всё придумал, пол-системы написали, а выкидывать и писать заново НА ОСНОВЕ ОПЫТА — не хотят (сроки/деньги и т.п. чушь). Был бы у каждой системы второй шанс — всё было бы намного лучше.

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

M>Был бы у каждой системы второй шанс — всё было бы намного лучше.

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

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

IT>Не вижу в твоём утверждении логической связи между тем, что после 'если' и после 'то'.

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

Здравствуйте, Ромашка, Вы писали:

IT>>Не вижу в твоём утверждении логической связи между тем, что после 'если' и после 'то'.
Р>"Сложность", по определению, это количество ошибок на километр кода.

Откуда такое "поопределение"?

Здравствуйте, IT, Вы писали:
Р>>"Сложность", по определению, это количество ошибок на километр кода.
IT>Откуда такое "поопределение"?

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

Здравствуйте, Ромашка, Вы писали:

Р>>>"Сложность", по определению, это количество ошибок на километр кода.
IT>>Откуда такое "поопределение"?
Р>У тебя есть другое, которое не сводится к ошибкам на километр? Озвучь, пожалуйста.

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

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

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

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

DG>тогда уж (если все-таки хочется инкапсуляцию)
DG>

DG>LazyMaker selectedElementMaker = new LazyMaker(()=>UpdateControl_ForSelectedElement(selectedElement.Control),
DG> delegate { return selectedElement; }
DG>);
DG>

Не вижу здесь никакой дополнительной инкапсуляции. Что изменилось-то от того, что ты код обработки вынес из LazyMaker'а в функцию этого же контрола?

DG>это Push, и имеет характерные проблемы связанные с Push.

Естественно Push. Каким это чудом у тебя на стыке с сеттерным кодом может быть Pull?

DG>в частности, тяжело подмешивать декораторы, например, что элементы на поле должны выводится дополнительно Italic-ом,
DG>а название элемента при наведении мышкой должен выводится синим (и это приоритетнее, чем вывод выделенности)

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

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

S>Что же до "доказательства верности программ", то я вообще слабо представляю, как математики, которые не решили проблемы, автоматического доказательства утверждений у себя, собираются помочь в этом программистам?

Очень просто, в программах большинство инвариантов, требующих доказательства, сводятся к примитивной арифметике и логике первого порядка, там автоматизированная проверка не представляет такой уж большой проблемы. Делая очередную опердень, теорему Гёделя не получишь. Кое-какие примеры на ATS я показывал тут, например реализация хитрой сортировки с машинно-проверенным доказательством того, что результат действительно отсортирован для любых входных данных, и что при работе с массивом 100% не будет выходов за его пределы (без рантайм-проверок!).

S>Где та методика у самих математиков — наваял Перельман доказательство — запихнули его в компьютер, или просто по листикам раздали студентам с "инструкцией выполнения" и опа — "доказательство верно!" или "доказательство неверно в такой строчке на такой-то странице!"

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

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

S>>Более обобщенно — какая "алфавитно"-символьная запись позволяет бороться с таким рассогласованием, и наоборот — позволяет быстро восстановить модель в уме человека?

DG>такая которая позволяет задачу восстановления модели поручить компьютеру.

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

Проблема в авторе — создавшем модель, записавшем ее.