Формальные доказательства это сложно. Это сложнее чем математические доказательства, потому что приходится писать на "математическом ассемблере"
Из личного опыта: я неделю потратил пытаясь доказать корректность частичной реализации printf (поддерживает только %u и %s). На обычном языке на написание и проверки времени бы ушло не более часа
В России у вас никто не отнимает права запускать, изучать, модифицировать код, поэтому ПО под свободной лицензией остаётся свободным.
Описаная в статье проблема касается только вирусных лицензий. Более того, существуют невирусные свободные лицензии, которые можно на законных основаних использовать в своём продукте не раскрывая исходный код
Вам ответили там, отвечу вам и здесь. Если лицензия запрещает пользоваться софтом людям/организациям которые вам не нравятся, он (софт) перестёт быть свободным. Об этом, кстати, даже сказано на странице проекта gnu
Слово "негр"-то вам чем не угодило? В русском языке оно негативного оттенка не имеет, просто представитель негроидной расы. Так же как европеец представитель европеоидной, эфиоп эфиопской и т.п.
От того, что неопределённое поведение описано в стандарте более адекватным оно не становится. Имхо: во-первых это грязнейший костыль, во-вторых инструмент должен помогать программисту, а не быть минным полем
Не вижу противоречия. Полезность распределённой платформы в данном случае определяется количеством узлов. Пока узлов мало, пользоваться платформой больно. Централизованный запуск просто позволяет сразу завлечь много людей и пропустить этап поедания кактуса
И всё же, несмотря на то, что рассуждения не полны, вывод правильный: предел последовательности, каждый член которой целый, не может быть не целым (±inf пределом не считаем)
Вы ведь понимаете, что комплексные числа вводятся не как ? Формально они определяются (один из способов) как пары , которые складываются и вычитаются покомпонентно, а умножение определено как
Вы можете привести хотя бы одно формальное определение для вашего деления на ноль?
С многозначной функцией проблемы ещё серьёзнее. Эта структура вообще перестаёт быть группой и у неё ломается куча свойств, например, x/y больше не равно x*(1/y), (a+b)/c не равно a/c + b/c
Комплексные числа интуитивны сами по себе, без контекста в виде уравнения прямой. Если ваше деление на ноль имеет смысл только в уравнении прямой, то это не более чем удобная запись. Числами в полной мере это не является
Действительные числа довольно интуитивно продолжаются комплексными. Однако, с делением на ноль совсем другая история. Если разрешить делить на ноль, получившаяся структура окажется до жути неинтуитивной
Я утверждаю, что вы не можете привести такую перестановку(биекцию) , что , и, более того, могу это доказать. Вам же достаточно привести одну такую функцию S, чтобы опровергнуть меня
В этом-то и дело, что чтобы убедить компилятор формально верифицированного языка нужно закапываться
Могу сразу сказать где у вас возникнут трудности:
"Если
A[i]" Доступ кA[i], нужно показать, чтоiкорректный индекс"не поменялись с прошлой итерации" -- итераций нет, нужно переделывать на рекурсию
"делается
swap" -- данные иммутабельные, нужно писать свой swap и доказывать, что все остальные элементы остались на своих местах"
j + 1" -- доказать, чтоj + 1корректный индекс"Числа до
j - 1остались с прошлой итерации" -- прошлой итерации нет, при рекурсии нужно требовать доказательство корректности входных данныхЕсли интересно -- я могу дать названия книг и несколько сайтов с формальными доказательствами. Можете попробовать оформить ваше доказательство
Тут пару лет назад доказывали, что gcd корректен. https://0xd34df00d.me/posts/2020/09/agda-wf-rec.html
Формальные доказательства это сложно. Это сложнее чем математические доказательства, потому что приходится писать на "математическом ассемблере"
Из личного опыта: я неделю потратил пытаясь доказать корректность частичной реализации printf (поддерживает только %u и %s). На обычном языке на написание и проверки времени бы ушло не более часа
В России у вас никто не отнимает права запускать, изучать, модифицировать код, поэтому ПО под свободной лицензией остаётся свободным.
Описаная в статье проблема касается только вирусных лицензий. Более того, существуют невирусные свободные лицензии, которые можно на законных основаних использовать в своём продукте не раскрывая исходный код
Давайте, я готов вступить с вами в дискуссию, но выскажите утверждение, которое вы будете отстаивать
Пример не чёткий, но думаю, вы подразумеваете, что бенефециар — владелец продукта Б
Софт А свободным быть не перестал. Софт Б, свободным и не был. Пока не заставят исполнять лицензию, софт Б и не будет свободным
Вам ответили там, отвечу вам и здесь. Если лицензия запрещает пользоваться софтом людям/организациям которые вам не нравятся, он (софт) перестёт быть свободным. Об этом, кстати, даже сказано на странице проекта gnu
Тоже было неожиданностью, но вот: https://ru.m.wikipedia.org/wiki/Эфиопская_раса
Слово "негр"-то вам чем не угодило? В русском языке оно негативного оттенка не имеет, просто представитель негроидной расы. Так же как европеец представитель европеоидной, эфиоп эфиопской и т.п.
От того, что неопределённое поведение описано в стандарте более адекватным оно не становится. Имхо: во-первых это грязнейший костыль, во-вторых инструмент должен помогать программисту, а не быть минным полем
Не вижу противоречия. Полезность распределённой платформы в данном случае определяется количеством узлов. Пока узлов мало, пользоваться платформой больно. Централизованный запуск просто позволяет сразу завлечь много людей и пропустить этап поедания кактуса
И всё же, несмотря на то, что рассуждения не полны, вывод правильный: предел последовательности, каждый член которой целый, не может быть не целым (±inf пределом не считаем)
Зависит от определения сечения. Я по тому что в википедии писал
Формально
это всё разные вещи.
Натуральная единица задана аксиомами Пеано
Целая единица это пара из знака и натуральной единицы
Рациональная единица это пара (числитель и знаменатель) из целой единицы и натуральной единицы
Действительная единица это вообще пара
И несмотря на эти отличия, мы спокойно используем различные числа вместе. Каждое множество погружается в следующее с сохранением всех операций.
Если честно, я не понимаю чем погружение действительных чисел в комплексные принципиально отличается
Вы ведь понимаете, что комплексные числа вводятся не как
? Формально они определяются (один из способов) как пары 
, которые складываются и вычитаются покомпонентно, а умножение определено как 
Вы можете привести хотя бы одно формальное определение для вашего деления на ноль?
Случайно минус вам влепил. Вернул плюсами в три других коммента
Векторное умножение обычно и не называют продолжением действительного
С многозначной функцией проблемы ещё серьёзнее. Эта структура вообще перестаёт быть группой и у неё ломается куча свойств, например, x/y больше не равно x*(1/y), (a+b)/c не равно a/c + b/c
Комплексные числа интуитивны сами по себе, без контекста в виде уравнения прямой. Если ваше деление на ноль имеет смысл только в уравнении прямой, то это не более чем удобная запись. Числами в полной мере это не является
Действительные числа довольно интуитивно продолжаются комплексными. Однако, с делением на ноль совсем другая история. Если разрешить делить на ноль, получившаяся структура окажется до жути неинтуитивной
Я утверждаю, что вы не можете привести такую перестановку(биекцию)
, что 
, и, более того, могу это доказать. Вам же достаточно привести одну такую функцию S, чтобы опровергнуть меня