соперников — C. Самого недостойного, т.к. в этом языке были нарушены все открытые к тому времени принципы серьезного программирования. Он запутывает студентов, допуская разный смысл для x = y и y = x и принуждая всех писать x = = y вместо обычного x = y. Только за одни эти
Здравствуйте, Дарней, Вы писали:
Д>господа, ну сколько уже можно? Д>ругать С — это пошло просто до безобразия
Наверное, покажусь неоригинальным, но C во многом безобразный язык. И == это самое меньшее, к чему можно было прицепиться. Впрочем, Pascal по-моему еще более безобразный язык. Д>тем не менее, им и его потомками пользовались, пользуются и будут пользоваться. Потому что ничего лучше пока не придумали. Языки, созданные
Э-э, шутить изволите? Придумали. При чем, еще до появления C. Д> теоретиками "на бумажке", почти никогда не оказываются востребованными — просто потому, что теоретики не имеют представления о реальных проблемах программирования и вместо этого борются с ветряными мельницами.
А реальные проблемы программирования на C/C++ возникают, в первую очередь, из-за самого языка. Начиная от банального if (a = b), и заканчивая порчей указателей, утечками памяти и прочими-прочими радостями. Да и сам по себе императивный подход к программированию удобен далеко не всегда. Временами, императивный подход очень сильно мешает. Д>А все разговоры о "порочном круге" — это просто паранойя. Появись язык, который реально, а не на словах лучше — все будут пользоваться именно им.
Один лемминг, что примечательно, ошибается куда реже миллионов.
P.S. Запомните: язык для задачи, а не задача для языка.
Здравствуйте, mihailik, Вы писали:
Ш>>>1) По мелочи. Вирт -- типичный лузер. Статья его -- просто жалкий вопль человека, проигравшего конкурентную борьбу. K_O>>Сначала неплохо бы сделать столько, сколько Вирт, а уж потом ярлыки клеить.
M>Если бы Вирт действовал так, как ты требуешь, у нас бы сейчас не было Паскаля.
Здравствуйте, kuj, Вы писали:
kuj>Впрочем, Pascal по-моему еще более безобразный язык.
странно
Д>>тем не менее, им и его потомками пользовались, пользуются и будут пользоваться. Потому что ничего лучше пока не придумали. Языки, созданные kuj>Э-э, шутить изволите? Придумали. При чем, еще до появления C.
и что это за язык и какой из них красивее?
kuj>А реальные проблемы программирования на C/C++ возникают, в первую очередь, из-за самого языка. Начиная от банального if (a = b), и заканчивая порчей указателей, утечками памяти и прочими-прочими радостями.
Здравствуйте, INTP_mihoshi, Вы писали:
INT>Здравствуйте, Шахтер, Вы писали:
INT>Месье не понимет
Месье как раз очень хорошо понимает в предмете.
Ш>>Возьмем, для примера, современную математику. Математика НЕ строится на базе какого-то формального языка. INT>Математика строится на основе формального языка.
Ага, вы это Арнольду скажите. Если успеете увернуться от летящей табуретки, то будете жить.
Ш>>Хотя технически это можно сделать, причем соответствующий язык будет попроще Паскаля. INT>Он вобще состоит только из одного правили — правила вывода одних теорем из других методом подстановки своюодных переменных.
Мда, курс мат. логики вам позорно читали.
Ш>>Вот только данный путь почему-то не привлекает никого. INT>Не знаю, привлекает или не привлекает, но _доказательства_ должны делаться только на нем. В _измышлениях_, разумеется, можешь пользоваться чем угодно.
Ш>>Потому что если так работать, то доказать можно будет разве что 2+2=4. INT>ВСЕ теоремы доказываются только так. Если, конечно, доказываются.
Ш>>Не годится такой подход для сложных задач. INT>Действительно сложные задачи решаются либо так, либо неправильно. Современное ПО как раз уперлось в предел сложности, который не перешагнуть без формального контроля правильности кода.
У меня большая просьба. Если вы действитнльно верите во всё вами написанное, то дайте формальное определение того языка, о котором вы говорили, покажите мат литературу, написанную на этом языке, ну и приведите пример какого-нибудь нетривиального доказательства, сделанного на этом языке.
Здравствуйте, Leonid V. Volnin, Вы писали:
LVV>On Wed, 12 May 2004 01:20:38 GMT, Шахтер <forum@rsdn.ru> wrote:
>> Здравствуйте, LaptevVV, Вы писали: >> >> LVV>http://www.inr.ac.ru/~info21/greetings/wirth_doklad_rus.htm >> >> 3) Попробую сформулировать свою мысль. Не уверен, что делаю это вполне >> ясно. >> Возьмем, для примера, современную математику. Математика НЕ строится на >> базе какого-то формального языка. Хотя технически это можно >> сделать, причем соответствующий язык будет попроще Паскаля.
LVV>можно я попридираюсь к мелочам? LVV>выделенная фраза очень сильно меня смущает: LVV>А как же теорема Гёделя? Что любая формальная система сложнее LVV>арифметики Пеано с равенством обязательно содержит парадоксы?
Теорема Гёделя ничего такого не утверждает. Она утверждает лишь, что или в языке будут противоречия, или он будет неполон, т.е. найдется утверждение, которое нельзя будет ни доказать, ни опровергнуть.
По поводу формального языка математики. Можно взять исчисление предикатов, соответствующим образом формилизованное (т.е. надо написать грамматику как минимум), и добавить к нему аксиомы Гёделя-фон Неймана. Ну и можно для полноты картины аксиому Гротендика об универсальном множестве. И это покроет современную математику.
Другой вопрос, что пользоваться этим будет невозможно никак.
LVV>как вы собираетесь компилировать код, который может содержать LVV>противоречия?
Здравствуйте, Дм.Григорьев, Вы писали:
ДГ>Здравствуйте, Шахтер, Вы писали:
Ш>>Вопрос на засыпку -- многие ли программисты знают, что такое интеграл Лебега?
ДГ>А какое это имеет отношение к флейму C++ vs other-shit?
Я имел ввиду, что чтобы пользоваться вот этим математически доказываемые системы наверно, придётся математику подучить. Просто чтобы хорошо понимать, что такое математическое доказательство и научиться их делать.
Здравствуйте, Sinclair, Вы писали:
S>Здравствуйте, Дарней, Вы писали: Д>>это всё замечательно звучит, но на практике люди имеют обыкновение ошибаться. Заниматься моделированием, составлением набора аксиом будут все те же люди. Вывод очевиден.... S>Видишь ли, шансов сделать ошибку тем меньше, чем меньше объем работы. Проверить корректность правил вывода достаточно легко, ибо их совсем немного. А дальше все происходит автоматически — ввели исходные аксиомы и получили заведомо правильные теоремы. Аксиом тоже относительно немного.
1) Позвольте уточнить, куда ввели и откуда получили.
2) Для справки. Есть такая формальная аксиоматическая теория -- формальная теория элементарной геометрии. Эта теория, как было доказано, разрешима -- т.е. существует алгоритм, который по любому утверждению этой теории может определить -- выводимо оно из аксиом или выводимо его отрицание.
Вот только одна проблема: сложность этого алгоритма -- двойная экспонента.
Здравствуйте, kuj, Вы писали:
kuj>Здравствуйте, Дарней, Вы писали:
kuj>Наверное, покажусь неоригинальным, но C во многом безобразный язык. И == это самое меньшее, к чему можно было прицепиться. Впрочем, Pascal по-моему еще более безобразный язык.
про Паскаль согласен. Вспоминаю про := и бегины с ендами, и сразу думаю "и эти люди запрещают мне ковыряться в носу?!"
Д>>тем не менее, им и его потомками пользовались, пользуются и будут пользоваться. Потому что ничего лучше пока не придумали. Языки, созданные kuj>Э-э, шутить изволите? Придумали. При чем, еще до появления C.
а можно с этого места и подробнее?
kuj>А реальные проблемы программирования на C/C++ возникают, в первую очередь, из-за самого языка. Начиная от банального if (a = b), и заканчивая порчей указателей, утечками памяти и прочими-прочими радостями. Да и сам по себе императивный подход к программированию удобен далеко не всегда. Временами, императивный подход очень сильно мешает.
я совсем не это имел в виду. К тому же, с появлением .NET это вроде бы разрешилось, хотя при большом желании накосячить можно и сейчас...
kuj>Один лемминг, что примечательно, ошибается куда реже миллионов.
вот как? очень интересная теория
kuj>P.S. Запомните: язык для задачи, а не задача для языка.
хто бы спорил. вот современные задачи и породили C с его потомками
Здравствуйте, beretta, Вы писали:
B>Здравствуйте, LaptevVV, Вы писали:
LVV>>http://www.inr.ac.ru/~info21/greetings/wirth_doklad_rus.htm
B>По слухам во французких школах преподают Ocaml. Может он не самый передовой, может из ФЯ как бейсик во времена моей школы (конец 80-х). Но все же показательно.
Из личного опыта взаимодействия с французскими программистами могу сделать вывод, что изучения Ocaml-а им не помогает
Д>>ругать С — это пошло просто до безобразия kuj>Наверное, покажусь неоригинальным, но C во многом безобразный язык. И == это самое меньшее, к чему можно было прицепиться.
Если ты хотел лишь сказать, что := лучше чем = а begin/end лучше скобок — то лучше бы и не начинал. Это не то, что стОит многодневных дискуссий.
kuj>А реальные проблемы программирования на C/C++ возникают, в первую очередь, из-за самого языка. Начиная от банального if (a = b), и заканчивая порчей указателей, утечками памяти и прочими-прочими радостями.
Я никак не дождусь одного: а кто же предложит рецепт избавления? Какие принципиальные новшества нужны для того, чтобы программист не ошибся, например, с выходом индекса за пределы массива?
Здравствуйте, mihailik, Вы писали:
M>А вообще я люблю всякие антигуманные методы доказательства. Ну, чтобы мозги сами за себя спотыкались, или же неконструктивные доказательства вроде Канторовской диагонали там.
Кстати, канторовская диагональ — чрезвычайно конструктивное доказательство. Грубо говоря, если кто-то утверждает, что перенумеровал все действительные числа на [0;1), то мы просим его оформить это гениальное открытие в виде функции int f(int i, int j), выдающей j-ю цифру после запятой у i-го числа. Диагональ задается как
int g(int i)
{
int result = f(i,i) == 4 ? 5 : 4;
assert(result != f(i,i));
assert(result != 0 && result != 9);
return result;
}
Здравствуйте, kuj, Вы писали:
kuj>Здравствуйте, Kh_Oleg, Вы писали:
K_O>>тем дольше время компиляции, kuj>Нет. C# сложнее, чем C++, а время компиляции программы на C# ниже. kuj>Время компиляции очень слабо связано со сложностью языка.
Неправильно оценивать сложность языка только количеством ключевых слов.
В C# разве есть шаблоны в том виде, в каком они есть в C++? Разве есть этот отстой в виде обычных, const, volatile и const volatile методов? То же и про переменные. А множественное наследование для классов?
Эти "фичи" на несколько порядков усложняют компилятор.
А здесь можно прочитать рассказ российских разработчиков о том, чего стоит написать компилятор С++.
K_O>>тем выше вероятность наличия "ловушек" в синтаксисе языка, kuj>Это вроде if (a = b) в C/C++?
ага, или double d = 3,1415;
K_O>>тем дольше время поиска ошибок kuj>C#/Java => C++ — где дольше время поиска ошибок?
В шаблонах никогда ошибок не искал? Компилятор всегда внятно может сказать, что и где ему не понравилось?
K_O>>и отладки, kuj>C#/Java => C++ — ...
См. предыдущий пункт.
K_O>>тем дольше общее время разработки, kuj>C#/Java => C++
На C++ время разработки на порядки дольше. Из-за времени компиляции. Много ты наотлаживаешься, когда проект собирается 45мин. ?
K_O>>тем выше себестоимость продукта... kuj>Не правда ваша. Себестоимость продукта зависит не от сложности языка, а от человекочасов, потраченных на ее написание, отладку, введение в эксплуатацию, документирование, поддержку, маркетинг (опционально) и т.д. и т.д.
документирование, поддержку, маркетинг (опционально) — это везде одинаково, а вот "человекочасы, потраченных на ее написание, отладку," напрямую зависят от сложности языка и времени компиляции.
Здравствуйте, INTP_mihoshi, Вы писали:
Ш>>Возьмем, для примера, современную математику. Математика НЕ строится на базе какого-то формального языка. INT>Математика строится на основе формального языка.
Кого начитался — Рассела, Бурбаки или Лема?
- Вы меняете взгляды чаще, чем подштанники! — крикнул обозленный, прямо-таки выведенный из социостатического равновесия лорд Поппер. — Скажи мне, лорд Рассел, что осталось у тебя от дивной поры молодой? Три тома "Principia Mathematica", вымученных за долгие годы. Так вот: спешу сообщить, что Чанг Вэнь или другой какой-нибудь Пинг-Понг — не запоминаю я этих китайских имен — запрограммировал компьютер так, что все доказанное Б.Расселом в его пресловутых "Принципах" машина доказала за восемь минут со средней скоростью самоубийцы, который бросился с девяностого этажа на Юпитере, где, как известно, сила тяжести во столько же раз больше земной, сколько раз домработница господина Тичи ошиблась в счетах из прачечной в свою пользу.
Первая попытка формализации математики (если не считать Фреге) была предпринята Расселом — "1+1=2" доказывается в теореме 110.643 на 83 странице второго тома. Его труд, как известно, не был продолжен.
Вторая попытка — Бурбаки, где число 2 вводится на странице 188 первого тома (в русском издании). но еще на странице 34 сказано, что "построение математики строго в соответствии с этим принципом привело бы к крайне длинным рассуждениям", и в метаматематических рассуждениях сразу же начинают применяться натуральные числа без строгого обоснования. Более того, во введении (стр. 28) изложена политика:
Но формализованная математика не может быть записана вся полностью, и потому в конце концов приходится питать доверие к тому, что можно назвать здравым смыслом математика, — доверие, аналогичное тому, которое бухгалтер и инженер, не подозревая о существовании аксиом Пеано, питают к формуле или численной таблице и которое в конечном счете основано на том, что оно никогда не было подорвано фактами.
...
Итак, написанный по аксиоматическому методу и сохраняющий всюду в виду, как некий горизонт, возможность полной формализации, наш Трактат претендует на полную строгость — претензия, которую не опровергают ни изложенные выше соображения, ни списки опечаток, с помощью которых мы исправляли и будем исправлять ошибки, время от времени вкрадывающиеся в текст.
Половина первого тома бурбаков и все дальнейшие тома по стилю слабо отличаются от обычной математической литературы.
Третья попытка — исследования последних двадцати лет с помощью доказывалок типа Coq или Isabelle/HOL. Формализм там совершенно другой — вместо теории множеств применяется функциональное программирование через изоморфизм Карри-Ховарда, и получено много интересных результатов, далеко выходящих за пределы проверки трех томов Рассела за восемь минут. Но до формализации, скажем, доказательства теоремы Ферма еще годы, если не десятилетия.
_>Кстати, канторовская диагональ — чрезвычайно конструктивное доказательство.
Конструктивное — это если бы он показал, почему действительные числа несчётны.
А он колупнул туда, колупнул сюда и нашёл противоречие. Голову надурил, а не подкопаешься. Получается, неконструктивное доказательство. Верное, но неконструктивное. Класс.
Здравствуйте, mihailik, Вы писали:
_>>Кстати, канторовская диагональ — чрезвычайно конструктивное доказательство. M>Конструктивное — это если бы он показал, почему действительные числа несчётны. M>А он колупнул туда, колупнул сюда и нашёл противоречие. Голову надурил, а не подкопаешься. Получается, неконструктивное доказательство. Верное, но неконструктивное. Класс.
А как можно доказать, например, что на моем столе нет листочка с неприличной картинкой? Взять каждую бумажку, посмотреть на нее и не найти ничего неприличного, потом из частных суждений сформировать общее. Тоже неконструктивно?
_>А как можно доказать, например, что на моем столе нет листочка с неприличной картинкой? Взять каждую бумажку, посмотреть на нее и не найти ничего неприличного, потом из частных суждений сформировать общее. Тоже неконструктивно?
Это как раз конструктивное.
Другое дело, что ты можешь взять свойства стола, необходимые для того, чтобы на нём лежали неприличные картинки, замутить обощение и привести к противоречию. Это уже неконструктивное доказательство.
Здравствуйте, mihailik, Вы писали:
_>>А как можно доказать, например, что на моем столе нет листочка с неприличной картинкой? Взять каждую бумажку, посмотреть на нее и не найти ничего неприличного, потом из частных суждений сформировать общее. Тоже неконструктивно? M>Это как раз конструктивное. M>Другое дело, что ты можешь взять свойства стола, необходимые для того, чтобы на нём лежали неприличные картинки, замутить обощение и привести к противоречию. Это уже неконструктивное доказательство.
Правильно. Но доказательство Кантора как раз первого вида. Мы хотим доказать, что не существует биекции между натуральными числами и [0;1). Для этого берем каждую функцию из первого во второе, внимательно смотрим на нее и говорим "ага, а вот этого-то числа здесь и не хватает! значит, не биекция". Как еще конструктивнее доказать, что чего-то не существует?
Начиная от банального if (a = b), и заканчивая порчей указателей, утечками памяти и прочими-прочими радостями. Да и сам по себе императивный подход к программированию удобен далеко не всегда. Временами, императивный подход очень сильно мешает.
Ньютон или Декарт? 
