Есть две программы на разных языках, обе реализуют один и тот же алгоритм. Как формально доказать, что для всех возможных входных данных они возвращают одинаковый результат? Очевидно, что с юнит-тестами тут облом. Это вообще возможно?pic random
ты изначально подумай, как доказать полную корректность хоть 1 программы?спойлер - формальная верификация. Вот если сделаешь это хоть для одной, для второй сделай так же
>>1536170На дваче таких вумников нет.мимо непонятно зачем потратил 2 месяца своей жизни на метаматематику и SF
>>1536166>спойлер - формальная верификацияДа знаю я, Агда-хуягда. Меня конкретика интересует, хотя бы на примере хелловорлд.
>>1536183Зачем тебе это? Если ты не вонабиматематик с мехмата - формально верифицировать программы тебе никто не даст. Это вход для избранных.
>>1536185Да хорош мозги ебать, это /зк или где? Есть конкретная прикладная задача, нужно не обосраться с новой версией программы.
>>1536187Ну можешь поиграть с трансформацией. Мол задаёшь эквивалентные структуры и сравниваешь.Если твои яп не поддерживают что-то такое из коробки то ты соснешь ибо сложно.Я так понимаю доступный для тебя способ верификации это банальные тесты.В чем проблема?В мёд исследованиях используют например метод двойной проверки, когда 2 программиста независимо пишут программу а потом сверяют результат.У тебя нечто ответсвеннее медицинских исследований?
>>1536241>В чем проблема?в том, что ты можешь написать хоть 1000 тестов, а на 1001-м появится разница в результатах, или на 100001-м, ну ты понел
>>1536241> метод двойной проверки, когда 2 программиста независимо пишут программу а потом сверяют результатесть, где об этом можно почитать? с исследованиями, хуе-мое
>>1536269Просто никто тут не мается такой далёкой от реальности хуитой, не имеющей никакого практического применения. Впрочем, кого я обманываю.
Если программы на разных яп, плохо дело. Чисто теоретически, если оба эти яп конпелируются в llvm, то стоит копать в сторону Coq + Vellvm/Crellvm. Агды хуягды сразу мимо, потому что такая задача требует для решения не только формализации яп, но и формализации самих анализируемых программ в виде элементов логики разделения (separation logic), а для агды все это придется писать самому, лол. В коке хотя бы что-то уже есть, хотя все равно придется дописывать. Я бы с такой задачей вообще связываться не стал, если речь не идёт о больших бабках.
>>1536241> Ну можешь поиграть с трансформацией. Мол задаёшь эквивалентные структуры и сравниваешь.> Если твои яп не поддерживают что-то такое из коробки то ты соснешь ибо сложно.А пример такого можно? В каких языках это есть?
>>1536187Для этого и существуют юнит-тесты. Старое зеленое, новое зеленое - значит работает. Недокументированные баги или непокрытый тестами случай - ну бывает, щито поделать.
>>1537018> ну бываетВот это ОПа и не устраивает, он хочет идеальную программу, которая гарантированно не имеет вообще ни одного бага. С такими спорить бесполезно.
>>1537018>значит работаетНихуя это не значит. Точнее, значит, что работает вот именно с этими данными, которые ты в тестах нахуярил.>>1537031>которая гарантированно не имеет вообще ни одного багаТы тупой? Нужна программа, которая работает так же как и старая. Ты читать вообще умеешь, макака ебаная?
>>1537033А стоит это затрат времени и сил на "гарантированно 100% копию программы"? Хорошо составленные юнит-тесты покроют тебе 99.9999% всех случаев, данные они ж не с балды, они обычно подчиняются какому-то закону, плюс краевые случаи там, тыры-пыры. Ну и представь, что исходная программа не идеальна, там где-то будет деление на ноль например при определенном входе. Тебе это тоже надо воспроизвести?
>>1537038Тест как-то помогают, да, но это какая-то поебень в 2019 году, неужели ничего нормального не придумали? Это как решать квадратное уравнение, пробуя брутфорсом разные значения, авось что подойдет. Пиздец.
>>1537040Скоро будут тебе квантовые вычисления, может будет профессия "квантовый тестировщик". А пока лучшее что ты можешь сделать не влезая в какой-то адский матан - полный брут на кластере из GPU.
>>1537042>адский матанТак посоветуй матан, епт. Может, там уже все придумали, а вы до сих пор свои тестики дрочите. Блять, почему у вас раздел такое говно?
>>1536160 (OP)"Доказать" в математическом понимании невозможно, потому что вне математики ты вообще хуй что-то докажешь, программы не исключение. Если тебе нужно подтверждение работы программы в практическом смысле, то два стула:1) Классические black-box юнит-тесты, если набор ожидаемых входных-выходных данных в алгоритме не слишком широкий и их в принципе можно засунуть в десяток тестов и не ебать себе мозги2) Тесты имплементации, когда ты прокидываешь между тестом и внутренностями алгоритма интерфейс и по шагам верифицируешь, что алгоритм выполняется как надо(выставляет на каждом шаге нужное значение и т.п). Обычно не стоит того, но со сложными алгоритмами это единственный способ их протестировать на 100%. https://blog.cleancoder.com/uncle-bob/2017/01/09/DiamondSquare.html
>>1538358Доказать-то можно. Программирование строится на информатике и алгоритмах, которые-таки имеют теоретические обоснования и доказательную базу. Но это не умаляет того, что ОП поставил себе ебически сложную и абсолютно бессмысленную задачу.
>>1538360На бумажке с установленным набором аксиом ты можешь доказать что угодно - это и есть суть математики. Но как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.
>>1538403>Но как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.Просто невероятно, какие же тут долбоебы сидят. Иди свой реакт дрочи, плебей.
>>1538486Это еще что, студентик, вот когда откроешь для себя принципиальную недоказуемость любой научной теории - так вообще охуеешь наверное.
>>1538403>Но как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.
>>1536160 (OP)>Есть две программы на разных языках, обе реализуют один и тот же алгоритм. Как формально доказать, что для всех возможных входных данных они возвращают одинаковый результат?Есть методы оценки и доказательства. Подозреваю их очень много. Этим занимается теория вычислимости. Она к сожалению в вывшем СССР слабо развита. Но труды есть, их много. Только их не просто гуглить, ибо ключевых слов тысячи. Есть также программные средства доказательства теорем, например Coq.Тут есть упоминаниеhttp://mk.cs.msu.ru/images/8/82/Thesis_Novikova.pdf
>>1538779>>1538836Что-то в голос, мамкины математики реально не в курсе, что в науке нет доказательств, только опровержения? Одна из главных причин кстати, по которым математика не классифицируется как наука. Но продолжайте, мне интересно послушать ваши шизоидные разрывы.
>>1538894Мань, еще раз, любая работающая с реальным миром наука не может ничего доказать просто по определению. Программы в каком мире исполняются, в реальном или на твоей бумажке, где ты их "доказал"?
>>1538888Иди уроки учи, школьник. И не забудь почитать книги: "Математическая логика" Чёрча и с таким же названием книга Гилберта.
>>1538403> как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.Ага, превращается в тыкву. Изоморфизм Карри-Говарда погугли, хотя все равно ничего не поймёшь.
>>1538944>>1539358То есть студенты матфака с обосранными штанами все равно не понимают, о чем именно речь и продолжают твердить себе "если на бумажке работает, то и в компьютере работает, вот попробуй на бумажку переписать структуру программы и тогда докажется". Я даже не знаю, каким еще более простым языком вам можно объяснить, давайте как детям:1) Компьютерная программа - это по сути научная теория, на бумаге она сформулирована охуенной доказуемой математикой, но работать ей приходится в ужасном реальном мире2) С реальным миром взаимодействовать можно только через эксперименты3) Эксперимент не может доказать никакую теорию, только опровергнуть4) Единственный способ взаимодействия с компьютерной программой, работающей в реальном мире - это эксперимент, а значит и доказать ее корректность нельзя.А теперь попрошу вместо стандартного пердежа рассказать, с каким именно пунктом вы несогласны и как предлагаете доказывать научные теории, я посмеюсь.
>>1539422Ты узколобый необразованный невежда. Есть автоматические системы докательства теорем: Coq, Agda, и т.п. Есть формальные языки, описывающие семантику, прагматику языков программирования, используя которые можно рассуждать о корректности программ.У тебя абсолютно нулевое знание математики. Для начала ознакомься как доказываются теоремы, и что такое аксиомы. Почитай Колмогорова, он хорошо описывает принципы изучения математики, метаматематики, и доказательства.
>>1539422Чё ты мне простыни своего крайне ценного школьного мнения пишешь, я сослался на совершенно конкретную вещь, попробуй погуглить и понять, что ты не самый умный. Хотя, шизику что-то доказывать, такое себе...
>>1539483Манюнь, речь не о математике, а о том, что вне математики доказательств нет. Я же не спорю, что на бумажке все прекрасно доказываются и что теоремы с аксиомами заебись. Но теорема и теория - это немного разные вещи, жаль, что ты этого понять никак не можешь. >>1539498Классная вещь, жаль только, что чтобы провести соответствие между между программой и ее мат. доказательством, программу сначала надо переписать на бумажку, то есть возвращаемся к началу. Зачем ты себе в штаны насерил?
>>1539505Господи, ещё один шизик. Сколько вас тут? Хотя, ещё бы время тратить на очередное чучело зумера, считающее, что умнее всех.
>>1539505Ты наркоман штоле, сука? Тебе же сказали, есть специальные дисциплины, знания, методы, и инструменты, для доказательства компьютерных программ. Убейся аб стену!
>>1539554>естьПокажи хоть один, который не полагается на "докажи корректность в голове/на бумаге, а потом перепиши в компьютер". Я думаю, ты запнешься еще на этапе "докажи, что переписал без опечаток".
>>1539574Ок, Мань. Вот смотри. Есть таблица умножения на бумаге, и есть счёты. Будет ли разница между вычислением на бумаге и на счетах? Далее, есть булева логика на бумаге и есть логические вентили в микросхеме. Будет ли разница между работой логических вентилей и такой же записью на бумаге? Тебе в рот ссать можно ещё очень и очень долго, мне просто лень приводить более сложные примеры.
>>1539608Я когда-то на луркморье прочитал что-то вроде правил демагога, и там говорилось, что это не тролль должен что-то доказывать, а доказывать должны ему, а он должен говорить, что доказательство - говно. Так что лучше бы не кормить его.
>>1539608>Будет ли разница между вычислением на бумаге и на счетах?define "вычисления на счетах" для начала. В отрыве от человека, который эти счет перекидывает и совершает все вычисления в уме, никаких "вычислений на счетах" нет. Так что давай аналогию получше, обсеря.>логические вентили в микросхемеУже лучше, теперь надо доказать, что микросхема не бракованная и что там ничего местами не перепутано. На бумажке напишешь, что процесс создания микросхемы шел по строгому алгоритму, а поэтому брака там быть не может?
>>1539620Ты читал, что я пишу? Разница будет в этих случаях или нет? Счёты и микросхема не бракованные.
>>1539767Что именно означает "не бракованные"? Что они идеальные? Или все-таки, что погрешность в допустимых значениях? Но если второе, то у тебя в итоге выйдет, что 1 = 1.0000000000001 = 0.9999999999999, это ты уже доказал в математике? И опять же, кто доказал, что они не бракованные и не примут вдруг неожиданное значение в одной из миллиарда комбинаций?
>>1539774Ок, давай иначе. Результат на бумаге и на счетах и на бумаге и микросхеме получился одинаковый. Что мы этим опровергли?
Раньше всегда удивлялся, почему шизики легко примут и будут отстаивать с пеной у рта очевидную шизу и бред вместо нормальной, простой понятной и доказанной теории. А потом понял - одному шизу ближе и понятнее маняидеи другого такого же шиза, но не нормального здорового человека. Потому что шизофренический уклад един, ШУЕ.
>>1539786Чтобы сравнить результат на счетах и результат на бумаге, результат на счетах нужно сначала перевести на бумагу или хотя бы в голову. Как ты собрался это сделать без погрешности?>>1539814Молодец, ты уже что-то начал понимать. Я очень рад, что ты изобрел программы, которые могут выполняться в более высоком измерении, но обычные люди пока еще дрочатся с микросхемами(а некоторые даже со счетами) и программы выполнять могут только на них. Так вот, повторяю вопрос - как ты докажешь корректность работы программы, если даже не можешь доказать, что ее среда выполнения работает корректно?
>>1539831>доказанной теорииТеория не бывает доказанной. Подтвержденной - да, но это разные вещи и подтвержденная миллиард раз теория может быть опровергнута одним экспериментом в любой момент. Этим науки и отличаются от математики, что непонятного?
>>1536160 (OP)Прогнать на одинаковых тестах и не трахать мозги. Доказательства это сложная тема, на которую нужно потратить не один год жизни.
>>1536160 (OP)1-й способ. Построчно. Берешь и сравниваешь каждую строчку, используя стандарты языков (определения типов данных, операций и т.д.). Если каждая строчка у двух программ делает одно и то же, то программы эквивалентны.2-й способ.Сравнить получающийся ассемблерный код. Если он одинаков у обеих программ, то они эквивалентны.
Мимо проходил, но парень который говорит, что доказать корректность программы нельзя прав. Особенно фразой, что теории через эксперименты можно только опровергнуть, а не доказать. сколько тестов не проводи. Вот вам Ньютон ебаный: 300 лет эксперименты проводили, любой ваш блядский набор тестов, но для скоростей <<с, и что, это доказывает, что Ньютон охуенно работает 100% доказан? Нет, нихуя, пришла СТО, которая показывает, что запихни другой набор тестов и Ньютон хуйца навернет. Как и может быть ваши программы, придумай другой способ их потестить. То, что не придуман тест, опровергающий что-то, не делает это доказанным. Математика работает с чистыми аксиомами, там нет таких вещей как погрешности и тд. Либо выводится из аксиом, либо нет. Да и даже там постоянно срачи: вон Атья вроде заебали доказательство, а теперь ещё иди найди в нем ошибку. И если не найдешь это не значит, что ее нет. Может и есть, может и нет. Нельзя короче мир 100% делить на чёрное и белое. А школьнику, который Колмогоровым своим кидается, рекомендую сначала сунц свой закончить, или лицей вышечки, или где он там, а потом уже рассуждать про математику и доказательства.
>>1548047>парень который говорит, что доказать корректность программы нельзя прав.Ты хоть бы почитал, что такое доказательство.
>>1543290бля, какой же ты долбоёб, твой способ на практике ни для одной пары квивалентных программ не выдаст что они эквивалентные.Ваще - задача алгоритмически неразрешимая, ОР пусть гуглит теорему Поста там, Мальцева, задачу останову, и прочее содержание первых трёх лекций курса мат логики
>>1548047У тебя такая каша в посте, жесть.Тесты не доказывают что в программе нет ошибок. В лучшем случае, они доказывают что они в программе есть. (с) Э.ДейкстраНо формальная верификация =/= тесты и ты явно не понимаешь как она работает. Ну а остальное в твоем посте - мешанина из философских проблем. Ты уверен что хочешь обсудить их здесь?Допустим Юм прав, проблема индукции, черные лебеди, причинно-следственные связи это вера, гроб гроб кладбище пидор. Но с другой стороны, у миллиардов людей есть компуктеры, в них доуища транзисретов и они каждую писесекунду отрабатывают согласно законам физики. Ты же не переживаешь, что сейчас в любой момент в твоей пекарне парочка из них начнет вести себя сверхъестественным образом? Понимаешь к чему я клоню, амиго? Мне вообще больше нравится трактовка Ч.С. Пирса, который говорит, что эксперимент действительно не позволяет узнать нам истину (т.к. объективной истины вообще не существует), но показывает что мы можем выполнять какое-то действие. По поводу смены парадигм, научных революций и т.д., так от открытий ТО или квантовой физики, что, устройства работающие на принципах классической механики перестали работать? Штука в том, что новые парадигмы обычно дополняют старые, а если где-то что и ломается, так это всякие принципиальные построения, абстрактные модели, а прикладная параша как работала так и будет работать.BE REAL, NIGGA.
