Уже всем давно понятно, что современные мейнстримовые языки должны умереть — у них абстракции текут; нет определенной формальной семантики, только стандарты "юридического" качества; ПО на них написанное без аннотирования, требующего работы на порядок бОльшей, чем затрачено на его написание, не допускает мало-мальски содержательного формального анализа.
Вопрос: а как вы представляете формальные ЯП, способные потеснить сегодняшний мейнстрим?
Я вот никак, по ряду причин:
1) Как уже упоминалоь где-то рядом, разработка ПО хорошо так специализирована. Что хорошо для "ПО на выброс", то не пойдёт в корпоратив и наоборот. Сегодняшний мейнстрим — жуткая солянка, где каждый язык хорош в своей нише и недостаточно силён, чтобы влезть в чужую.
1.1) На самом деле, слегка неправильно вообще говорить только об ЯП в контексте "кто кого заборет". Сопутствующий toolset и возможность взаимодёйствия с внешним API зачастую куда важнее всех фишек языка, особенно если mind model не совпадают.
2) Мейнстрим такой мейнстрим — либо решаем насущные задачи быстро/легко/дёшево/поддерживаемо (нужное зачеркнуть), либо в мейнстрим не лезем. А из насущных задач у нас что?
а) докрутить TUniversalComponent до рабочего состояния
б) автоматизировать бардак
в) как бы изловчиться и пнуть чужую систему чтобы она заработала.
г) найти ошибку в сложной логике с кучей условий и неочевидным code flow.
Как тут помогут формальные ЯП — хз.
2.1) Единственный почти декларативный мейнстримовый язык — SQL — хорошо показывает результат "хорошая идея vs суровая действительность".
3) Практически весь "свежий мейнстрим" — либо императивщина + чуть-чуть фп, либо декларативные высокоуровневые протоколы/стандарты описания данных (читай XML). На описание семантики никто не замахивается. Т.к. много их, ваших семантик. Плюс потихоньку пролазит декларативщина на низкий уровень, главным образом для описания state-машин (описание драйверов в сингулярити, Axum)
4) Если посмотреть на "мейнстрим из завтра", то у нас чётко видно 2 направления: виртуализация чего только можно и смесь DSL с императивщиной. На "формальная модель->код" никто пока не замахивается.
5) Возможность формальной валидации тьюринг-полного языка очень и очень сомнительна из-за нереальной размерности пространства состояний и слишком сложной формальной модели (по сравнению с реализацией "в лоб").
5.1) Валидность формальной модели вовсе не означает отсутствие ошибок в алгоритме, т.е. решающего превосходства формального подхода что-то не видно.
. Чтобы не оффтопить, вынес сюда.
S>Исходный посыл (deniok): S>
S>Уже всем давно понятно, что современные мейнстримовые языки должны умереть — у них абстракции текут; нет определенной формальной семантики, только стандарты "юридического" качества; ПО на них написанное без аннотирования, требующего работы на порядок бОльшей, чем затрачено на его написание, не допускает мало-мальски содержательного формального анализа.
S>Вопрос: а как вы представляете формальные ЯП, способные потеснить сегодняшний мейнстрим?
S>Я вот никак, по ряду причин:
[...]
Перенос этой ветки сюда, в философию, причём в виде выделенной цитаты, превращает мою маленькую провокацию в большой наброс. Мой тезис был в том, что бессмысленно говорить о формальном анализе и верификации текстов современных программ; языки на которых они написаны слишком бедны для этого. Чтобы справиться с задачей требуются существенные трудозатраты на аннотирование кода на специальных вспомогательных языках. Например, для Java есть проект Krakatoa в котором такие аннотации пишутся на специальном языке JML.
Я сильно сомневаюсь к тому же, что такое аннотирование вообще применимо к сколько-нибудь существенной части уже написанного кода. Что ещё более увеличивает трудности формального анализа и верификации.
Будут ли массовые языки становится более податливыми к формальным методам? Думаю будут, этот процесс идет, низкоуровневые инструменты широкого спектра действия с неопределяемой из их применения семантикой (вроде кастинга указателей в стиле C, да и самих указателей) изгоняются из языков.
С другой стороны, большинство интересных универсальных систем формальной верификации построены на использовании богатых систем типов. Теория, лежащая в основе систем типов ML с наследниками и Haskell — та же, что и для COQ, Agda и Epigram. Она сложна, но продуктивна в конструктивном смысле. Язык зависимых типов применим для того, чтобы записывать любые формальные требования к программе, причем весьма компактно. Проблема здесь в том, что опыта мало и пока непонятно, какие тИповые примитивы и механизмы связи (код-тип) зашивать в язык, а что делать через библиотеки. Но то, что отлаженные вкусняшки будут с какой-то задержкой перекочевывать в мейнстрим можно не сомневаться.
Здравствуйте, Sinix, Вы писали:
S>Вопрос: а как вы представляете формальные ЯП, способные потеснить сегодняшний мейнстрим?
Никак себе не представляю мэйнстримный (т.е. достаточно распространённый и устойчиво занимающий свою нишу) формальный ЯП.
Кроме того, не очень чётко себе представляю, что это такое — формальный ЯП. По-видимому, формальный ЯП и функциональный ЯП — это, всё таки разные вещи.
Есть большие сомнения, что математика, основанная на теории множеств, в принципе может быть полезна при синтезе и для анализа больших и сложных систем (если кому интересна аргументация, об этом немножко есть ближе к концу вот этого моего опуса). Соответственно, не исключено, что так и не удастся никогда изобрести какой-то реально полезную при разработке ПО аксиоматику, основанную на теории множеств.
На низком уровне у нас всё ОК. Булева алгебра и цифровые автоматы — это наше всё. Когда же дело доходит до чего-то реально большого и сложного... включаем интуицию, и "нашим всем" становится уже опыт, сын ошибок гнусных.
Здравствуйте, Voblin, Вы писали:
V>Есть большие сомнения, что математика, основанная на теории множеств, в принципе может быть полезна при синтезе и для анализа больших и сложных систем (если кому интересна аргументация, об этом немножко есть ближе к концу вот этого моего опуса). Соответственно, не исключено, что так и не удастся никогда изобрести какой-то реально полезную при разработке ПО аксиоматику, основанную на теории множеств.
Есть альтернатива теории множеств, как фундаменту CS, -- теория категорий.
Здравствуйте, deniok, Вы писали:
D>Есть альтернатива теории множеств, как фундаменту CS, -- теория категорий.
на сколько я понимаю теория категорий сама формулируется в терминах теории множеств.
Здравствуйте, cvetkov, Вы писали:
C>Здравствуйте, deniok, Вы писали:
D>>Есть альтернатива теории множеств, как фундаменту CS, -- теория категорий. C>на сколько я понимаю теория категорий сама формулируется в терминах теории множеств.
Нет, её аксиоматика независима от теории множеств. Категория малых множеств Set или понятие конкретной категории — всего лишь частные случаи.
Здравствуйте, deniok, Вы писали:
D>Что-то по-русски ничего не найти. По-английски ключевые слова Domain Theory, Type Theory, Cartesian Closed Categories, Topos theory.
Качнул "Введение в теорию категорий и функторов" товарищей Букур и Деляну. На первый взгляд: чистое сумасшествие. Игра в бисер. Как вплести эти кракозябры в структуру реальности — ХЗ полное
Есть что-нибудь типа "Теория категорий для чайников"? С примерами. Чтобы чисто конкретно хотя бы с чем-то соотнести эти двести страниц птичьего языка.
Господи, благодарю Тебя, что все нужное Ты сделал простым, а все сложное — ненужным
Григорий Сковорода
Возник резонный вопрос: всё это великолепие вообще имеет хоть какую-то практическую или познавательную ценность или это всё чисто для того, чтобы почесать свой мозг?
Здравствуйте, Voblin, Вы писали:
V>Возник резонный вопрос: всё это великолепие вообще имеет хоть какую-то практическую или познавательную ценность или это всё чисто для того, чтобы почесать свой мозг?
Здравствуйте, deniok!
D>Перенос этой ветки сюда, в философию, причём в виде выделенной цитаты, превращает мою маленькую провокацию в большой наброс.
Не, большой — это если бы в КСВ%) А так хоть что-то можно обсуждать — обуждение вендеписца что-то поднадоело.
D> Мой тезис был в том, что бессмысленно говорить о формальном анализе и верификации текстов современных программ; языки на которых они написаны слишком бедны для этого.
Это так.
D> Чтобы справиться с задачей требуются существенные трудозатраты на аннотирование кода на специальных вспомогательных языках. Например, для Java есть проект Krakatoa в котором такие аннотации пишутся на специальном языке JML.
На первый взгляд — продвинутые code assertions с возможностью статической верификации (аналогично code contracts 4 фреймворка). Что-нить упустил?
D>Будут ли массовые языки становится более податливыми к формальным методам?
Не думаю. Дело в том, что assertions семантически никак не связаны с кодом который они покрывают. Всё что здесь можно сделать — довести синтаксис до юзабельного состояния, но, в любом случае, аннотации-инварианты всегда будут выглядеть этакими костылями к императивному коду.
D>С другой стороны, большинство интересных универсальных систем формальной верификации построены на использовании богатых систем типов. ... Проблема здесь в том, что опыта мало и пока непонятно, какие тИповые примитивы и механизмы связи (код-тип) зашивать в язык, а что делать через библиотеки.
А вы не ставите телегу впереди коня? Мне всегда казалось, что формальная верификация удобна благодаря зависимым типам, а не наоборот. И неплохо бы сначала сам ФП окончательно сделать частью мейнстрима, а затем уже замахиваться на нечто большее. Иначе так и останется вся эта прелесть вариться в собственном котле.
Про "что в код, а что в библиотеки". Если присмотритесь к мейнстриму, то количество языковых конструкций стараются сокращать до минимально разумного, а затем добавлять синтаксический сахар для отдельных фич (для сложных вещей добавляя целый DSL). Проблема здесь не в языке, а в сопутствующих библиотеках и рантайме. Полноценная поддержка любых концептуальных изменений — это очень большая работа, которая потенциально затрагивает все сопутствующие библиотеки. А вот профит (как оно есть сейчас) очень и очень сомнителен.
Здравствуйте, Voblin!
V>Кроме того, не очень чётко себе представляю, что это такое — формальный ЯП. По-видимому, формальный ЯП и функциональный ЯП — это, всё таки разные вещи.
Формальный ЯП — это такая сферическая штука, к которой предъявляется как минимум одно требование — можно доказать валидность кода, т.е. его соответствие требуемому поведению. Разумеется, вариантов "как это сделать" выше крыши, но, поскольку ФП выглядит заумнее (и только потому что имеет другую mind model), обычно все смотрят именно в эту сторону. Что слегка нечестно, т.к. в чистом ФП и так достаточно сделано для потенциальной формализуемости.
В первую очередь, это stateless кода. Как следствие — отсутствие side effects, что сводит на нет целый класс ошибок. Во-вторых, в ФП удобно описывать вычислительные алгоритмы — которые сами по себе относительно легко верифицируются. И, в третьих, ФП не очень-то и сталкивается со всеми прелестями разработки корпоративного ПО и его развитие почти никак им не покорёжено.
Тепличные условия, так сказать.
V>Есть большие сомнения, что математика, основанная на теории множеств, в принципе может быть полезна при синтезе и для анализа больших и сложных систем.
Теория множеств мегаштука. Но она абсолютно бессильно перед самой мейнстримной задачей — автоматизировать бардак из-за бесконечного числа инвариантов. Не буду расписывать, у меня уже пальцы отваливаются.
V>Когда же дело доходит до чего-то реально большого и сложного... включаем интуицию, и "нашим всем" становится уже опыт, сын ошибок гнусных.
От-от-от. Ибо сложные системы (равно как и жисть вообще) штука абсолютно неформализуемая и непредсказуемая. Максимум, что можно сделать — это составить инструкции по выполнению каких-то действий, не описывая их формально. Потому что объём информации, необходимый для валидации этих действий хорошо так превышает объём самих инструкций.
Здравствуйте, Voblin, Вы писали:
V>Есть большие сомнения, что математика, основанная на теории множеств, в принципе может быть полезна при синтезе и для анализа больших и сложных систем (если кому интересна аргументация, об этом немножко есть ближе к концу вот этого моего опуса).
Тема опуса интересная, но вот содержание слишком наивное.
1. Насчет "Как это ни удивительно звучит, но почему-то никто не обратил особого внимания на то, что математика создана и развита нами, людьми": животные тоже умеют пользоваться арифметикой, даже муравьи это делают.
2. Математика не может опираться на понятие справедливости, т.к. само это понятие опирается на математику и невозможно без нее.
3. По поводу "Предметов, свойства которых изучает эта наука, в реальном мире не существует" и "Земля вокруг Солнца летит по эллиптической орбите, но такой штуки как эллипс, в природе не существует" — наивно полагать, что Земля более реальна, чем эллипс. С одной стороны, все познаваемое уже существует (с т.з. матлогики), с другой стороны, Земля — такая же абстрактная концепция, всего лишь человеческий ярлык для большого скопления элементов, каждый из которых — тоже не более, чем концепция. Как говорил Бор, "вещи, которые мы считаем реальными, сделаны из вещей, которые мы не можем считать реальными". Короче, это отдельная большая тема...
4. Про кибернетику и "приемлемого математического аппарата для описания процессов управления (и в живом мире, и в технике, и в обществе) не существует вообще" — есть ведь денотационная и операционные семантики, есть теория оптимального управления. Вполне математично, точно и без всякой статистики. Высокая сложность — да, есть такая проблема. Но никто чудес и не обещал, "математика 2.0" вряд ли эту сложность уменьшит.
Здравствуйте, Voblin, Вы писали:
V>Качнул "Введение в теорию категорий и функторов" товарищей Букур и Деляну. На первый взгляд: чистое сумасшествие. Игра в бисер. Как вплести эти кракозябры в структуру реальности — ХЗ полное
Как раз на эту тему, всего 70 страниц: http://math.ucr.edu/home/baez/rosetta.pdf
Самая интересная математическая книжка, которую мне доводилось читать. Там теория категорий позволяет увидеть прямые параллели в CS, топологии, квантовой физике и логике. Написана для широкого читателя, весьма доходчиво, знаний ТК не требуется.
V>На низком уровне у нас всё ОК. Булева алгебра и цифровые автоматы — это наше всё. Когда же дело доходит до чего-то реально большого и сложного... включаем интуицию, и "нашим всем" становится уже опыт, сын ошибок гнусных.
Это точно, по научному это звучит как "задача трассировки требований к проекту". Т.е. менеджер вносит изменения, а программист должен быстро-быстро исправить код. Очевидно может быть более чем два уровня, но задача эта нерешабельная силами существующих средств. Тут происходит именно это — включаем интуицию и вперед!
Случайно открыл язык програмирования более абстрактный чем ЯВУ на основе ООП. Страшно подумать, но повышение уровня абстрактности не связано с выдумыванием понятий более сложных чем UML. Думаю вы просто не поверите. имхо вместо решения проблемы "формальная модель->код" нужно на другие проблемы обращать внимание: каким образом программист выбирает интерфейс, производит декомпазицию системы и почему ООП не позволяет использование нескольких архитектур в одном проекте?
Больше всего меня поразил один факт: оказывается полная инкапсуляция не защищает реализацию от изменений. Тут больше всего проявляется бесполезность чистого формализма при решении проблем в программировании. Для математика очевидно, что отделив формально интерфейсом часть от остальной системы мы можем делать с реализацией что нам захочеться. Т.е. как бы получаем свободу действий. На самом деле требование по изменению интерфейса нарушает всю эту математическую идилию. Вывод математика справедлив только для одного заданного интерфейса, а на другие интерфейсы и на смену интерфейсов не распространяется. Та же ситуация прослеживается ври задании схемы наследования объектов, выбора абстрактных уровней и т.д. и т.п. везде где хоть в каком то виде происходит деление целого на части.
Здравствуйте, D. Mon, Вы писали:
DM>Здравствуйте, Voblin, Вы писали:
V>>Есть большие сомнения, что математика, основанная на теории множеств, в принципе может быть полезна при синтезе и для анализа больших и сложных систем (если кому интересна аргументация, об этом немножко есть ближе к концу вот этого моего опуса).
DM>Тема опуса интересная, но вот содержание слишком наивное. DM>1. Насчет "Как это ни удивительно звучит, но почему-то никто не обратил особого внимания на то, что математика создана и развита нами, людьми": животные тоже умеют пользоваться арифметикой, даже муравьи это делают.
DM>2. Математика не может опираться на понятие справедливости, т.к. само это понятие опирается на математику и невозможно без нее.
DM>3. По поводу "Предметов, свойства которых изучает эта наука, в реальном мире не существует" и "Земля вокруг Солнца летит по эллиптической орбите, но такой штуки как эллипс, в природе не существует" — наивно полагать, что Земля более реальна, чем эллипс. С одной стороны, все познаваемое уже существует (с т.з. матлогики), с другой стороны, Земля — такая же абстрактная концепция, всего лишь человеческий ярлык для большого скопления элементов, каждый из которых — тоже не более, чем концепция. Как говорил Бор, "вещи, которые мы считаем реальными, сделаны из вещей, которые мы не можем считать реальными". Короче, это отдельная большая тема...
DM>4. Про кибернетику и "приемлемого математического аппарата для описания процессов управления (и в живом мире, и в технике, и в обществе) не существует вообще" — есть ведь денотационная и операционные семантики, есть теория оптимального управления. Вполне математично, точно и без всякой статистики. Высокая сложность — да, есть такая проблема. Но никто чудес и не обещал, "математика 2.0" вряд ли эту сложность уменьшит.
Здравствуйте, D. Mon, Вы писали:
DM>Тема опуса интересная, но вот содержание слишком наивное.
Чем богаты, тем и рады
DM>1. Насчет "Как это ни удивительно звучит, но почему-то никто не обратил особого внимания на то, что математика создана и развита нами, людьми": животные тоже умеют пользоваться арифметикой, даже муравьи это делают.
"Пользоваться" может и что, и кто угодно. Камень тоже "пользуется" параболой, когда летит к земле. Что-то я сильно сомневаюсь, что муравьи развлекаются самым главным, что есть в математике — доказательством утверждений. А то, что они друг другу могут передавать информацию, по своей сути являющуюся числами и умеют эти самые числа складывать, меня не очень удивляет. Матушка-эволюция и не такие навороты умеет наворачивать.
DM>2. Математика не может опираться на понятие справедливости, т.к. само это понятие опирается на математику и невозможно без нее.
Понятие справедливости не может опираться на математику. Например, моя собака очень чётко понимает, что справедливо, а что нет. И когда вдруг оказывается несправедливо наказана или чем-то обделена, обижается. То же самое с маленькими детьми. Трёхлетнему карапузу не нужен никакой из математических разделов, чтобы мгновенно разобраться, что вставать в угол за совершенно случайно разлитое молоко — несправедливо.
DM>3. [...] Как говорил Бор, "вещи, которые мы считаем реальными, сделаны из вещей, которые мы не можем считать реальными". Короче, это отдельная большая тема...
Тема эта действительно очень большая и забавная. Называется "дуализм бытия и сознания".
DM>4. Про кибернетику и "приемлемого математического аппарата для описания процессов управления (и в живом мире, и в технике, и в обществе) не существует вообще" — есть ведь денотационная и операционные семантики, есть теория оптимального управления. Вполне математично, точно и без всякой статистики. Высокая сложность — да, есть такая проблема. Но никто чудес и не обещал, "математика 2.0" вряд ли эту сложность уменьшит.
Конечно, есть методы. И теории. Всякие. У них, правда, есть одно неприятное свойство: на уровне всякой мелкой элементарщины они прекрасно работают и весьма удобны, но при увеличении сложности работоспособность и удобство катастрофически падают.
Вот и получается такая фигня: информационные технологии, всей своей сутью предназначенные для борьбы со сложностью, основаны на теориях, которые с увеличением сложности превращаются во что-то совсем невразумительное.
А со сложностью не нужно бороться. С ней нужно сотрудничать. Её нужно использовать. А для этого нужно знать, каким образом можно использовать сложность в своих целях. Пока же единственное действие, которое мы знаем применительно к сложности — это её редукция.
Математика 2.0 в том числе нужна и как теоретический базис для инфотехнологий 2.0, которые научатся не только делать инструменты произвольной (т.е. адекватной задаче) сложности, но и помогут организовывать сложный (а других, собственно и не бывает) процесс так, чтобы и цель достигалась, и "побочные эффекты" не расфигачили всё вокруг.
Чудес не надо. Надо, чтобы были способы делать так, чтобы всё было абсолютно естественно и было как можно меньше "чудес".
Здравствуйте, Sinix, Вы писали:
S>Формальный ЯП — это такая сферическая штука, к которой предъявляется как минимум одно требование — можно доказать валидность кода, т.е. его соответствие требуемому поведению.
Не возникает ли здесь логической петли? Чтобы доказать соответствие кода требуемому поведению, нужно иметь и код, и формализованное требуемое поведение. А чтобы доказать валидность формализации требуемого поведения, нужно... что? Ну да, нужна гиперсферическая штука, которая использует тот же принцип для доказательства валидности формализованных требований требуемому поведению. И так до бесконечности.
S>В первую очередь, это stateless кода. Как следствие — отсутствие side effects, что сводит на нет целый класс ошибок.
Это очень хорошо, когда этот самый stateless допустим. То есть целью работы не является нечто обратное ему (какой-нибудь stateness).
Знаю, знаю про монады в ФП...
S>Во-вторых, в ФП удобно описывать вычислительные алгоритмы — которые сами по себе относительно легко верифицируются.
О! В этом вся суть самого главного ограничения. Т.е. задача должна быть в принципе сводима к схеме "начали — пока работаем, всё пофиг — кончили". В жизни это обычно не так.
S>И, в третьих, ФП не очень-то и сталкивается со всеми прелестями разработки корпоративного ПО и его развитие почти никак им не покорёжено. S>Тепличные условия, так сказать.
Интересно было бы узнать, почему?
S>Теория множеств мегаштука. Но она абсолютно бессильно перед самой мейнстримной задачей — автоматизировать бардак из-за бесконечного числа инвариантов. Не буду расписывать, у меня уже пальцы отваливаются.
Вопреки распространённому мнению, автоматизировать бардак можно и нужно. Там, где нет бардака, там и без автоматизации всё хорошо.
Для того, чтобы автоматизировать хаос, нужна просто немножко необычная система автоматизации. Хаотическая . Жёлтенькие стикеры + калькулятор + ворд + эксель — вот инструменты, на базе которых можно строить систему автоматизации любого бардака.
S>От-от-от. Ибо сложные системы (равно как и жисть вообще) штука абсолютно неформализуемая и непредсказуемая. Максимум, что можно сделать — это составить инструкции по выполнению каких-то действий, не описывая их формально. Потому что объём информации, необходимый для валидации этих действий хорошо так превышает объём самих инструкций.
Может быть, мы просто пока не умеем готовить этих кошек?
Здравствуйте, Voblin, Вы писали:
DM>>животные тоже умеют пользоваться арифметикой, даже муравьи это делают. V>"Пользоваться" может и что, и кто угодно. Камень тоже "пользуется" параболой, когда летит к земле. Что-то я сильно сомневаюсь, что муравьи развлекаются самым главным, что есть в математике — доказательством утверждений. А то, что они друг другу могут передавать информацию, по своей сути являющуюся числами и умеют эти самые числа складывать, меня не очень удивляет. Матушка-эволюция и не такие навороты умеет наворачивать.
Арифметика — часть математики, так что способность птиц и муравьев к счету уже лишает ее статуса чисто человеческого изобретения. Более абстрактная математика — теория множеств, логика и т.д. — это лишь формализация мышления, ничего чисто антропного там нет.
DM>>2. Математика не может опираться на понятие справедливости, т.к. само это понятие опирается на математику и невозможно без нее. V>Понятие справедливости не может опираться на математику. Например, моя собака очень чётко понимает, что справедливо, а что нет. И когда вдруг оказывается несправедливо наказана или чем-то обделена, обижается. То же самое с маленькими детьми. Трёхлетнему карапузу не нужен никакой из математических разделов, чтобы мгновенно разобраться, что вставать в угол за совершенно случайно разлитое молоко — несправедливо.
Тут путаница понятий. Справедливо — это когда поровну, когда эквивалентно, т.е. чисто математическая штука. А описанные выше явления ближе к "незаслуженно" чем к "несправедливо", там совсем другое, основанное на привычках и эмоциях.
V>Конечно, есть методы. И теории. Всякие. У них, правда, есть одно неприятное свойство: на уровне всякой мелкой элементарщины они прекрасно работают и весьма удобны, но при увеличении сложности работоспособность и удобство катастрофически падают.
Здравствуйте, D. Mon, Вы писали:
DM>Арифметика — часть математики, так что способность птиц и муравьев к счету уже лишает ее статуса чисто человеческого изобретения. Более абстрактная математика — теория множеств, логика и т.д. — это лишь формализация мышления, ничего чисто антропного там нет.
Ага. А ещё собака, ловящая в прыжке летящую тарелку, по ходу дела решает кучу дифуров, описывающих движение тарелки и движение самой собаки. Дифуры — тоже часть математики. Лишим дифуры статуса чисто человеческого изобретения?
DM>Тут путаница понятий. Справедливо — это когда поровну, когда эквивалентно, т.е. чисто математическая штука. А описанные выше явления ближе к "незаслуженно" чем к "несправедливо", там совсем другое, основанное на привычках и эмоциях.
Справедливо — это не обязательно поровну. И не обязательно эквивалентно. Справедливость — это соблюдение договора.
При этом в качестве договора может быть что угодно — и собственно договор, и устное соглашение, и обещание, и писанный закон, и неписанный закон (так называемый общественный договор), и... да что угодно. В любом случае, вступая в любые отношения я рассчитываю на то, что в этих отношениях есть некие правила, которые будут соблюдены. Когда они соблюдаются, это справедливость. Когда они нарушаются — это несправедливость.
И что? Где здесь математика? Сплошные привычки, эмоции, иллюзии, обманутые надежды и прочая хрень.
Скажу пару слов по поводу договора. Я могу что угодно ворчать по поводу несправедливости правил преферанса. Десять в гору за каждую взятку на мизере — это ж чудовищно! Не годится! Но если я сел играть (добровольно вступил в отношения), я должен признать, что правила преферанса справедливы.
V>>Конечно, есть методы. И теории. Всякие. У них, правда, есть одно неприятное свойство: на уровне всякой мелкой элементарщины они прекрасно работают и весьма удобны, но при увеличении сложности работоспособность и удобство катастрофически падают. DM>Я и говорю — есть, но не без проблем.
Я тоже говорю, что можно даже протянуть железнодорожную ветку на Луну. Но не без проблем.
. Жёлтенькие стикеры + калькулятор + ворд + эксель — вот инструменты, на базе которых можно строить систему автоматизации любого бардака.