_>Как еще конструктивнее доказать, что чего-то не существует?

Вроде бы ты прав. Здорово объегорил!

Подумаю ещё на досуге. Надо же, как оно выходит...

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

Д>>>ругать С — это пошло просто до безобразия
kuj>>Наверное, покажусь неоригинальным, но C во многом безобразный язык. И == это самое меньшее, к чему можно было прицепиться.
SWW>Если ты хотел лишь сказать, что := лучше чем = а begin/end лучше скобок — то лучше бы и не начинал. Это не то, что стОит многодневных дискуссий.
Нет, я вовсе не это хотел сказать. Сравнивать языки сравнением операторных скобок все-равно что сравнивать оптимизации при компиляции программы "Hello world".

kuj>>А реальные проблемы программирования на C/C++ возникают, в первую очередь, из-за самого языка. Начиная от банального if (a = b), и заканчивая порчей указателей, утечками памяти и прочими-прочими радостями.
SWW>Я никак не дождусь одного: а кто же предложит рецепт избавления?
Рецептов избавления много и существуют они далеко не первый год. Просто Вы, наверное, ничего кроме пары императивных языков вроде C/C++/Pascal не видели. Например, все вышеуказанное в .NET языках в принципе не возможно (кроме как по вине ошибки в JIT-компиляторе или сборщике муссора). А сборщики муссора существовали еще в первых версиях LISP (который, кстати, во много раз старше C/C++/Pascal).
SWW>Какие принципиальные новшества нужны для того, чтобы программист не ошибся, например, с выходом индекса за пределы массива?
Проверка на выход за границы массива существовала еще в Delphi. В .NET ественно она тоже существует.

kuj>Рецептов избавления много и существуют они далеко не первый год. Просто Вы, наверное, ничего кроме пары императивных языков вроде C/C++/Pascal не видели. Например, все вышеуказанное в .NET языках в принципе не возможно (кроме как по вине ошибки в JIT-компиляторе или сборщике муссора). А сборщики муссора существовали еще в первых версиях LISP (который, кстати, во много раз старше C/C++/Pascal).

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

Не могу сказать, что я с этим на 100% согласен, но что-то в этом есть.

SWW>>Какие принципиальные новшества нужны для того, чтобы программист не ошибся, например, с выходом индекса за пределы массива?
kuj>Проверка на выход за границы массива существовала еще в Delphi. В .NET ественно она тоже существует.

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

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

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

kuj>>Рецептов избавления много и существуют они далеко не первый год. Просто Вы, наверное, ничего кроме пары императивных языков вроде C/C++/Pascal не видели. Например, все вышеуказанное в .NET языках в принципе не возможно (кроме как по вине ошибки в JIT-компиляторе или сборщике муссора). А сборщики муссора существовали еще в первых версиях LISP (который, кстати, во много раз старше C/C++/Pascal).

SWW>Есть мнение, что наличие сборщика мусора расслабляет программиста, он относится к программе легкомысленно, что приводит к появлению программ с уродской архитектурой. А отсутствие сборщика мусора заставляет программиста точно представлять себе сроки жизни каждого объекта, благодаря чему он тщательнее продумывает архиректуру своей программы что в конечном итоге идет ему на пользу.

SWW>Не могу сказать, что я с этим на 100% согласен, но что-то в этом есть.

Одного человека спросили:

— Почему Вы всегда переходите улицу на красный свет?
— Чтоб не расслабляться.

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

Ш>И в программировании мы наблюдаем то же самое. C++ гораздо более подходит для создания больших и сложных систем, чем всякие Жабы. И я думаю, дальше будет только хуже в этом смысле. Эволюция языков программирования будет идти в сторону сложности и меньшей формальности. Прямо в противоположном направлении, которое хочет тов. Вирт.
Только Net и Ява предлагает другую концепцию уменьшающую количество ошибок, скорость разработки и читабельность кода. А это направление как раз созвучно словам Вирта. Причем Net позволяет писать более простые компиляторы в MSIL код, и соответственно появление различных языков решающие различные задачи не загорами.

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


>Но до формализации, скажем, доказательства теоремы Ферма еще годы, если не десятилетия.

А что вы понимаете под "формализацией доказательства теоремы Ферма"?? Она уже давно доказана. Причем строго математически. Или вы что-то другое имеете ввиду??

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

LVV>> Я вижу в своем воображении образцовый учебник в качестве подходящего исходного пункта. Он должен удовлетворять следующим критериям:
LVV>>Начинаться сжатым введением в основные понятия программного проектирования.
LVV>>Использовать лаконичную формальную нотацию, строго определенную не более чем на примерно 20 страницах.
SWW><...>
SWW>Глупости. Это был бы худший учебник, какой только можно придумать. Он был бы понятен только тому, кто уже знает язык.
SWW>Практика же показывает, что лучший учебник — это Керниган-Ритчи, который безо всяких формальных нотаций с первой же страницы предлагает писать простую программу.
Вы не путайте обучение кодированию на конкретном языке программирования с обучением, собственно, самому программированию, которое, вообще говоря, в идеале не должно привязываться к конкретному языку программирования.

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

ДГ>>Ругать и обсуждать — разные вещи. А в языке действительно масса проблем. Если ты считаешь, что это не так, значит ты просто мало писал на нем и не пробовал другие языки. Попробуй поработать на Java: имхо он гораздо лучше чем C++ (сама идеология языка, сырые библиотеки не в счет), на столько же, насколько C++ лучше старого паскаля.
Д>Ява? не смешите мои тапочки
Д>Из-за отсутствия шаблонов,
Шаблоны уже есть. Они конечно далеки от идеала по части реализации (т.к. пораждают overhead), но они есть.

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

_>Здравствуйте, Шахтер, Вы писали:

Ш>>Вопрос на засыпку -- многие ли программисты знают, что такое интеграл Лебега?

_>Изоморфизм Карри-Ховарда и основы теории категорий для обсуждаемых целей полезнее

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

Копай Нео, копай -- летать научишься. © Matrix. Парадоксы

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

Обучение самому программированию? Вопрос, конечно, интересный и даже актуальный — но как учить самому программированию не изучив хотя бы один язык программирования? Как можно учить столяра делать мебель, не научив его пользоваться ножовкой и рубанком?

Здравствуйте, Larm, Вы писали:
L> А что вы понимаете под "формализацией доказательства теоремы Ферма"?? Она уже давно доказана. Причем строго математически. Или вы что-то другое имеете ввиду??
Ну, насчет "давно" ты преувеличиваешь. А речь идет о формальном изложении доказательства не на естественном языке, а на специальном формальном языке.

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

>>Но до формализации, скажем, доказательства теоремы Ферма еще годы, если не десятилетия.
L> А что вы понимаете под "формализацией доказательства теоремы Ферма"?? Она уже давно доказана. Причем строго математически.

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

Вот, к примеру, Annals of Mathematics, 141(1995), страница 542:

As the semistable hypothesis implies that all the inertia groups outside 3 in the splitting field of rho_0 have order dividing 3 this means that the splitting field of rho_0 is unramified outside 3. However, Q(sqrt(-3)) has no nontrivial abelian extensions unramified outside 3 and of order prime to 3. So rho_0 itself would factor through an abelian extension of Q and this is a contradiction as rho_0 is assumed odd and irreducible.

Кто возьмется формально доказать правильность этих слов с помощью "правил вывода одних теорем из других методом подстановки свободных переменных"?

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

INT>>Месье не понимет
Ш>Месье как раз очень хорошо понимает в предмете.
Теперь вижу


Ш>>>Не годится такой подход для сложных задач.
INT>>Действительно сложные задачи решаются либо так, либо неправильно. Современное ПО как раз уперлось в предел сложности, который не перешагнуть без формального контроля правильности кода.

Ш>У меня большая просьба. Если вы действитнльно верите во всё вами написанное, то дайте формальное определение того языка, о котором вы говорили, покажите мат литературу, написанную на этом языке, ну и приведите пример какого-нибудь нетривиального доказательства, сделанного на этом языке.

Я не говорю, что формальное выведение применяют всегда as is. Формальное выведение — это как ассемблер для программирования. Ассемблер сам по себе применяют редко, но если мы хотим, чтобы программа выполнялась, то она должна быть выразима через него.

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

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

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

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

У программистов есть компиляторы, а у математиков (пока?) нет. Интересно, школьник, изучающий ершол без компьютера, тоже пишет в конечном счете на ассемблере, даже если ни разу в жизни не написал синтаксически правильной программы? Учитель, конечно, может собрать тетради и дома проверить, но и ему свойственно ошибаться. Вот примерно в таком положении и находится сейчас математика, подтверждение тому — списки опечаток к учебникам (например, в еррате алгебры Dummit&amp;Foote 10 ошибок найдены мной).

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

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

_>У программистов есть компиляторы, а у математиков (пока?) нет.

Во-первых, APS (задолбало меня писать "системы автоматичесого жоказательства") на эту роль претендуют. Во-вторых, можно из одних теорем делать другие и использовать уже их. Вполне так себе ФЯ

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

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

_>Вот примерно в таком положении и находится сейчас математика, подтверждение тому — списки опечаток к учебникам (например, в еррате алгебры Dummit&amp;Foote 10 ошибок найдены мной).

А это к вопросу о том, нужно ли использование формальных доказательств

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

_>>У программистов есть компиляторы, а у математиков (пока?) нет.
INT>Во-первых, APS (задолбало меня писать "системы автоматичесого жоказательства") на эту роль претендуют.

Да, но это только начало пути. Библиотека coq-8.0/theories/Reals еще очень далека даже от первого курса матана.

INT>Во-вторых, можно из одних теорем делать другие и использовать уже их. Вполне так себе ФЯ

Это и есть основная идея изоморфизма Карри-Ховарда.

_>>Вот примерно в таком положении и находится сейчас математика, подтверждение тому — списки опечаток к учебникам (например, в еррате алгебры Dummit&amp;Foote 10 ошибок найдены мной).
INT>А это к вопросу о том, нужно ли использование формальных доказательств

Конечно, нужно. Только вот арифметика и геометрия существуют больше двух тысяч лет, алгебра (Виет, Декарт) и теория чисел (Ферма) — 400, анализ (Ньютон) — 300, абстрактная алгебра (Абель, Галуа) — 180, теория множеств (Кантор) и топология (Пуанкаре) — 100. По принципу "действительно сложные задачи решаются либо так, либо неправильно" объявим все их результаты неправильными?

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

_>>>У программистов есть компиляторы, а у математиков (пока?) нет.
INT>>Во-первых, APS (задолбало меня писать "системы автоматичесого жоказательства") на эту роль претендуют.

_>Да, но это только начало пути. Библиотека coq-8.0/theories/Reals еще очень далека даже от первого курса матана.

С одной стороны, да. А с другой язык С++ наполовину состоит из APS. Так что, если рассматривать APS как средство написания программ, то они уже давно и широко используются.

INT>>А это к вопросу о том, нужно ли использование формальных доказательств

_>Конечно, нужно. Только вот арифметика и геометрия существуют больше двух тысяч лет, алгебра (Виет, Декарт) и теория чисел (Ферма) — 400, анализ (Ньютон) — 300, абстрактная алгебра (Абель, Галуа) — 180, теория множеств (Кантор) и топология (Пуанкаре) — 100. По принципу "действительно сложные задачи решаются либо так, либо неправильно" объявим все их результаты неправильными?

Ну, они же теперь формально доказаны? Значит, формально правильны

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

INT>С одной стороны, да. А с другой язык С++ наполовину состоит из APS. Так что, если рассматривать APS как средство написания программ, то они уже давно и широко используются.

Нет. Настоящая APS извлекает код из доказательства спецификации программы. Например, на 271 странице документации к Coq (http://coq.inria.fr) разобран пример извлечения алгоритма сортировки из доказательства теоремы о том, что любой массив некоей перестановкой превращается в отсортированный. В contribs к Coq есть таким же образом доказанные алгоритмы Хаффмана и Бухбергера. К непонятно какой половине C++ это отношения не имеет.

_>>Только вот арифметика и геометрия существуют больше двух тысяч лет, алгебра (Виет, Декарт) и теория чисел (Ферма) — 400, анализ (Ньютон) — 300, абстрактная алгебра (Абель, Галуа) — 180, теория множеств (Кантор) и топология (Пуанкаре) — 100.
INT>Ну, они же теперь формально доказаны?

Нет. Только очень малая часть.

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

INT>>С одной стороны, да. А с другой язык С++ наполовину состоит из APS. Так что, если рассматривать APS как средство написания программ, то они уже давно и широко используются.

_>Нет. Настоящая APS извлекает код из доказательства спецификации программы. Например, на 271 странице документации к Coq (http://coq.inria.fr) разобран пример извлечения алгоритма сортировки из доказательства теоремы о том, что любой массив некоей перестановкой превращается в отсортированный. В contribs к Coq есть таким же образом доказанные алгоритмы Хаффмана и Бухбергера. К непонятно какой половине C++ это отношения не имеет.

К контролю типов, константности методов, корректности инициализации, прав доступа.

Скажем, для того, чтобы объявить метод константным, нужно формально доказать, что все используемые в нем операции также являются константными. При этом можно добавлять акиому о правильности некоторого метода ключевым через const_cast. Правда, новых тактик добавлять нельзя

Между прочим, ты не сравнивал Hol, Isabella и Coq? В чем они отличаются и насколько они совместимы?

_>>>Только вот арифметика и геометрия существуют больше двух тысяч лет, алгебра (Виет, Декарт) и теория чисел (Ферма) — 400, анализ (Ньютон) — 300, абстрактная алгебра (Абель, Галуа) — 180, теория множеств (Кантор) и топология (Пуанкаре) — 100.
INT>>Ну, они же теперь формально доказаны?

_>Нет. Только очень малая часть.

Значит, еще не известно, правильны они или нет.

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

INT>Скажем, для того, чтобы объявить метод константным, нужно формально доказать, что все используемые в нем операции также являются константными. При этом можно добавлять акиому о правильности некоторого метода ключевым через const_cast. Правда, новых тактик добавлять нельзя

Ага, система доказательства, умеющая доказывать только одну теорему — что программа синтаксически правильна. Она даже не может доказать или опровергнуть, что при выполнении не возникнет undefined behavior и что выполнение вообще завершиться.

INT>Между прочим, ты не сравнивал Hol, Isabella и Coq? В чем они отличаются и насколько они совместимы?

Я работал только с Coq. А у кого-нибудь еще есть windows-версия?

_>>>>Только вот арифметика и геометрия существуют больше двух тысяч лет, алгебра (Виет, Декарт) и теория чисел (Ферма) — 400, анализ (Ньютон) — 300, абстрактная алгебра (Абель, Галуа) — 180, теория множеств (Кантор) и топология (Пуанкаре) — 100.
INT>>>Ну, они же теперь формально доказаны?
_>>Нет. Только очень малая часть.
INT>Значит, еще не известно, правильны они или нет.

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