Исходное сообщение
"На соревновании Pwn2Own 2023 продемонстрировано 5 взломов Ub..." Отправлено Аноним, 27-Мрт-23 12:19
Формально доказывается отсутствие UB и ошибок с памятью. Это теоретически можно доказать даже на C'шном коде, и даже _формально_ доказать, но это настолько сложно, что никто не занимается этим. И всё сводится к "верю/не верю": либо ты веришь программисту, что он достаточно долго разглядывал каждую строчку своего кода, чтобы выловить всех блох, либо ты не веришь ему. Последнее время этот подход выходит из моды, потому что пришло понимание, что верить нельзя никому. 100% программистов совершают ошибки, и при этом, как ты правильно говоришь, есть подковёрная возня целенаправленно внедряющая такие ошибки. Хочется всё же иметь возможность доказывать утверждения о коде. И тщательный выбор языка может сделать формальное доказательство _существенно_ проще. Теоретически сам факт того, что программа написана на подобранном формальном языке и при этом компилируется и работает, может быть таким доказательством. Но это другая теоретическая крайность, потому что такие языки оказываются непрактичными. На практике люди выбирают компромисс: язык который способствует тому, чтобы про код возможно было бы доказывать утверждения доказательствами, которые на порядки короче кода, о котором они рассуждают, но при этом с минимумом палок в колёса задаче написания кода. А доказательство "злого умысла" по-хорошему никого не волнует как раз потому, что оно непрактично. Мало того, что сложно доказать, так ещё даже в случае успеха, это будет очень специфичным доказательством, которое доказывает что-либо о конкретном коммите, и ничего не говорит о следующем коммите. Но даже если бы оно было возможным, то останутся неумышленные ошибки. Поэтому на умысел все забивают, вообще забивают на эту идею доверия программисту, и переходят на модель недоверия программисту, стремясь максимально упростить проверку кода на безбажность. Чтобы нам не надо было бы верить в безбажность кода, чтобы мы могли бы проверить эту безбажность. Долой религию, да здравствует эмпиризм!

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:	> Формально доказывается отсутствие UB и ошибок с памятью. Это теоретически можно доказать > даже на C'шном коде, и даже _формально_ доказать, но это настолько > сложно, что никто не занимается этим. И всё сводится к "верю/не > верю": либо ты веришь программисту, что он достаточно долго разглядывал каждую > строчку своего кода, чтобы выловить всех блох, либо ты не веришь > ему. > Последнее время этот подход выходит из моды, потому что пришло понимание, что > верить нельзя никому. 100% программистов совершают ошибки, и при этом, как > ты правильно говоришь, есть подковёрная возня целенаправленно внедряющая такие ошибки. > Хочется всё же иметь возможность доказывать утверждения о коде. > И тщательный выбор языка может сделать формальное доказательство _существенно_ проще. > Теоретически сам факт того, что программа написана на подобранном формальном языке > и при этом компилируется и работает, может быть таким доказательством. Но > это другая теоретическая крайность, потому что такие языки оказываются непрактичными. > На практике люди выбирают компромисс: язык который способствует тому, чтобы про код > возможно было бы доказывать утверждения доказательствами, которые на порядки короче кода, > о котором они рассуждают, но при этом с минимумом палок в > колёса задаче написания кода. > А доказательство "злого умысла" по-хорошему никого не волнует как раз потому, что > оно непрактично. Мало того, что сложно доказать, так ещё даже в > случае успеха, это будет очень специфичным доказательством, которое доказывает что-либо > о конкретном коммите, и ничего не говорит о следующем коммите. Но > даже если бы оно было возможным, то останутся неумышленные ошибки. Поэтому > на умысел все забивают, вообще забивают на эту идею доверия программисту, > и переходят на модель недоверия программисту, стремясь максимально упростить проверку > кода на безбажность. Чтобы нам не надо было бы верить в > безбажность кода, чтобы мы могли бы проверить эту безбажность. Долой религию, > да здравствует эмпиризм!
	Введите код, изображенный на картинке: