Вариант для распечатки		Пред. тема | След. тема
Форум Разговоры, обсуждение новостей
Изначальное сообщение		[ Отслеживать ]

"Аnthropic развивает технику для формальной верификации существующего ПО при помощи AI"	+/–
Сообщение от opennews (??), 23-Окт-26, 10:41
Компания Аnthropic представила результаты экспериментов по использованию AI-моделей для формальной верификации надёжности и безопасности уже существующих проектов. В ходе эксперимента при помощи AI-моделей для 123 открытых библиотек, протестированных в инфраструктуре OSS Fuzz, были сгенерированы математические доказательства отсутствия ошибок при работе с памятью... Подробнее: https://www.opennet.ru/opennews/art.shtml?num=66528
Ответить | Правка | Cообщить модератору

Сообщения

[Сортировка по времени | RSS]

3. "Аnthropic развивает технику для формальной верификации сущес..."	–7 +/–
Сообщение от pic (??), 23-Окт-26, 10:47
Очень быстро ИИ опуститься до уровня машинных кодов и библиотеки, тулкиты, фреймворки станут бесполезны.
Ответить | Правка | Наверх | Cообщить модератору

	8. "Аnthropic развивает технику для формальной верификации сущес..."	+3 +/–
	Сообщение от Аноним (8), 23-Окт-26, 10:59
	Хоть какая-то польза от ИИ. Очистить ПО ландшафт от наслоившегося мусора в виде фреймворков, жабаскрипта, раста и всякой питонщины.
	Ответить | Правка | Наверх | Cообщить модератору

	75. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (75), 23-Окт-26, 13:38
	От фреймворков - не дождётесь.
	Ответить | Правка | Наверх | Cообщить модератору

	113. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (113), 23-Окт-26, 15:32
	Но первой удалят Сишечку.
	Ответить | Правка | К родителю #8 | Наверх | Cообщить модератору

	154. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (154), 23-Окт-26, 19:24
	> Хоть какая-то польза от ИИ. Очистить ПО ландшафт от наслоившегося мусора в виде ...в видебиомассы программистов азазазаза!
	Ответить | Правка | К родителю #8 | Наверх | Cообщить модератору

	227. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (227), 24-Окт-26, 11:25
	И не только. Потому что все эти программисты нанимались часто аутсорсом со всего мира. Денежная масса распределялась. И тратилась в т.ч. в бедных странах. А теперь она будет концентрироваться в странах с профи., с высоким образованием, где у людей есть время учитьсяа не добывать еду. То есть западных странах у нескольких гениев с ии.
	Ответить | Правка | Наверх | Cообщить модератору

	10. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 11:02
	Останутся только чисто функциональные языки, запомните этот твит!
	Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

	37. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от pic (??), 23-Окт-26, 12:11
	Тогда придётся и дальше плодить оптимизирующие компиляторы. Зачем? Тут два варианта, либо ИИ опускается до машинных кодов и быстрому портированию. Либо процессоры нужно переводить с машинных кодов на исполнение кода функционального языка. Подсказывать не буду.
	Ответить | Правка | Наверх | Cообщить модератору

	49. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (10), 23-Окт-26, 12:45
	Функциональщина поможет составлять непротиворечивые промпты. ИИ сама будет основана на этом языке. Нейро символические ИИ.
	Ответить | Правка | Наверх | Cообщить модератору

	47. "Аnthropic развивает технику для формальной верификации сущес..."	–2 +/–
	Сообщение от Боевой Петух (?), 23-Окт-26, 12:31
	Не останется вообще никаких языков, кроме промптинга. Уже через пару лет ИИ будет генерировать машинный код напрямую и коНпилятор станет не нужОн. Запомните этот твит.
	Ответить | Правка | К родителю #10 | Наверх | Cообщить модератору

	52. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:05
	Если составлять промпты, как ты пишешь комментарии, то на выходе получится ещё хуже, чем у джуна на C/C++
	Ответить | Правка | Наверх | Cообщить модератору

	101. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (101), 23-Окт-26, 14:33
	Но гораздо дешевле. А качество софта волнует не тех, кто его пишет, а тех, кто его использует. Так что всё правильно он написал.
	Ответить | Правка | Наверх | Cообщить модератору

	240. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от zehiu (?), 24-Окт-26, 18:39
	и зачем нам его запоминать? никогда не понимал этого выражения. ты, похоже, надеешься заслужить хоть какую-то кроху уважения к себе, когда потом выяснится, что одно из 100500 твоих предсказаний сбылось?
	Ответить | Правка | К родителю #10 | Наверх | Cообщить модератору

	12. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Ы (?), 23-Окт-26, 11:07
	Посмотри на «прибыль» антропик. Очень скоро может может пузырь лопнет и все опять вернутся к услугам кожаных мешков
	Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

Часть нити удалена модератором

	64. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (64), 23-Окт-26, 13:20
	Ну несколько лет назад биткойн постоянно лопался, теперь вот ИИ.
	Ответить | Правка | К родителю #240 | Наверх | Cообщить модератору

	124. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (113), 23-Окт-26, 16:16
	А что, Биткоин генерировал астрономические убытки? Обожаю аналитику на опенке.
	Ответить | Правка | Наверх | Cообщить модератору

	149. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 18:55
	> А что, Биткоин генерировал астрономические убытки? Обожаю аналитику на опенке. У кого-то генерировал
	Ответить | Правка | Наверх | Cообщить модератору

	35. "Аnthropic развивает технику для формальной верификации сущес..."	–4 +/–
	Сообщение от pic (??), 23-Окт-26, 12:07
	В произношении инфинитив не всегда ощущается по мягкому произношению. Скорее по ударению, но и ударение тоже бывает одинаковым при спряжении. Поэтому старые правила, что по советской реформе, что до неё, создают двойные стандарты. Нужна новая реформа.
	Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

	103. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Пыщь (?), 23-Окт-26, 14:35
	Старые правила написания инфинитивов однозначные (и там не по произношению). Не фантазируй, хотя продолжай наяривать невросети, своей эрудиции и образования lim->0.
	Ответить | Правка | Наверх | Cообщить модератору

	82. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (82), 23-Окт-26, 13:44
	ИИ считать нормально не умеет. Скрипты для этого пишет. Путается в перенумерации текстовых документов даже со скриптами, а ты про бинарники. Что бы такое делать надо держать модель процессора внутри модели ИИ. Сейчас нет таких механизмов, что бы создавать такие структуры. И никто даже не начинал работать в этом направлении.
	Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

	97. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 14:09
	Модель riscv проца с базовым набором инструкций не сильно больше модели языка brainfuck
	Ответить | Правка | Наверх | Cообщить модератору

	224. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (224), 24-Окт-26, 10:07
	brainfuck: Каждый символ — это готовая команда. Декодирование отсутствует. С эти текущий ИИ работать умеет. Он на такое заточен. RISC-V: Каждая инструкция — это 32-битное число. Эмулятору нужно программно "разобрать" этот 32-битный код: выделить тип инструкции (opcode), понять, какие регистры используются (rs1, rs2, rd), и извлечь непосредственное значение (immediate), которое к тому же может быть разбросано по разным битам ради оптимизации железной архитектуры. А вот с этим - нет. И то это будет RVI. И до RVA как до луны раком.
	Ответить | Правка | Наверх | Cообщить модератору

	125. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (113), 23-Окт-26, 16:18
	"что бы" пишет раздельно, но все ИИ критикует...
	Ответить | Правка | К родителю #82 | Наверх | Cообщить модератору

	260. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Прохожий (??), 25-Окт-26, 12:11
	Что бы ты ни делал, всё плохо. Здесь - раздельно. Чтобы писать правильно, надо учиться. Здесь - слитно.
	Ответить | Правка | Наверх | Cообщить модератору

	136. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от pic (??), 23-Окт-26, 18:02
	Кучер сравнивает Теслу со своей повозкой.
	Ответить | Правка | К родителю #82 | Наверх | Cообщить модератору

	223. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (224), 24-Окт-26, 09:57
	> Кучер сравнивает Теслу со своей повозкой. Назови мне модуль в ИИ который отвечает за вычисления.
	Ответить | Правка | Наверх | Cообщить модератору

	156. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (154), 23-Окт-26, 19:32
	> ИИ считать нормально не умеет. Ты из танка-то вылези. ИИка вон недавно порешала более 300 математических задач, над которыми лучшие математики планеты тщетно бились десятилетиями. Включая уравнения Навье-Стокса. А вашу корявую кучу г*кода не осилит, ага...
	Ответить | Правка | К родителю #82 | Наверх | Cообщить модератору

	222. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (224), 24-Окт-26, 09:56
	> Ты из танка-то вылези. ИИка вон недавно порешала более 300 математических задач, над которыми лучшие математики планеты тщетно бились десятилетиями. Включая уравнения Навье-Стокса. Ты хочешь сказать что ИИ считать умеет без скриптов?
	Ответить | Правка | Наверх | Cообщить модератору

	255. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (255), 25-Окт-26, 02:09
	Конечно, ошибается он в очень больших числах, не влезающих в int. Но и там он может применить алгебру, в которой он давно превзошел человека.
	Ответить | Правка | Наверх | Cообщить модератору

	259. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (259), 25-Окт-26, 12:10
	> Конечно, ошибается он в очень больших числах, не влезающих в int. Но и там он может применить алгебру, в которой он давно превзошел человека. Ты не пользуешься ИИ.
	Ответить | Правка | Наверх | Cообщить модератору

	254. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (254), 25-Окт-26, 01:13
	Люди тоже без калькулятора часто ошибаются даже с простой арифметикой. А на ассемблере пишут. тем не менее...
	Ответить | Правка | К родителю #82 | Наверх | Cообщить модератору

	147. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 18:29
	> Очень быстро ИИ опуститься до уровня машинных кодов и библиотеки Rocq Prover это уже машинный код у тебя?
	Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

	193. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Джон Титор (ok), 23-Окт-26, 23:02
	> Очень быстро ИИ опуститься до уровня машинных кодов и библиотеки, тулкиты, фреймворки станут бесполезны. Ну я делаю такую агентную систему. И скажу что вы не правы. Это невероятно энергозатратно сразу делать код ассемблера. Поэтому языки выского уровня никуда не денутся по причине того что это менее энергозатратно, а вот что случится с языками высокого уровня? Вот это интересный вопрос, потому что они могут превратится в языки среднего уровня, а наверх вылезти что-то другое. Уже сейчас есть множество сервисов предлагающие свои услуги. Но это потому что люди которые этим разобщены и хотят денег. А я уже чувствую бесполезность идеи превратить всё сразу в ассемблер. Но так... для демки покатит.
	Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

5. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
Сообщение от Аноним (5), 23-Окт-26, 10:50
тэк, огромадные специалисты в бям (больших языкастых моделях) если бинарный файл собирается из одного исходника, но с разными параметрами оптимизации например, бям верифицирует конкретную сборку, или всё же логику исходного кода?
Ответить | Правка | Наверх | Cообщить модератору

	9. "Аnthropic развивает технику для формальной верификации сущес..."	+5 +/–
	Сообщение от Аноним (10), 23-Окт-26, 10:59
	Что такое логика исходного кода? Особенно, когда на таких языках как C/C++ каждая вторая строчка это UB? На процессоре выполняется машинный код, его и надо верифицировать, а не какие то влажные мечты Васяна написанные на дырявом языке.
	Ответить | Правка | Наверх | Cообщить модератору

	15. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Ы (?), 23-Окт-26, 11:09
	Начать надо с верификации верилога процессора. А то окажется что там напортачили со спекулятивным исполнением инструкций 🤷♂
	Ответить | Правка | Наверх | Cообщить модератору

	17. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
	Сообщение от Аноним (10), 23-Окт-26, 11:12
	Поэтому и проверяют на riscv, где есть железо без этого барахла
	Ответить | Правка | Наверх | Cообщить модератору

	39. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
	Сообщение от Аноним (39), 23-Окт-26, 12:19
	А есть и с барахлом. RISC-V — это ISA, а не реализация (и в этом смысле в плане уязвимостей много хуже, т.к. несколько десятков производителей вам такой их феерический набор произведут).
	Ответить | Правка | Наверх | Cообщить модератору

	53. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:06
	С барахлом станет никому не нужно. Концепция поменяется
	Ответить | Правка | Наверх | Cообщить модератору

	41. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (41), 23-Окт-26, 12:23
	> железо без этого барахла Железо без этого оказалось не очень востребованным на рынке.
	Ответить | Правка | К родителю #17 | Наверх | Cообщить модератору

	51. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (10), 23-Окт-26, 12:50
	Потому что кожаные не могут придумывать подходящий для железа лайаутинг данных и алгоритмы их обработки
	Ответить | Правка | Наверх | Cообщить модератору

	88. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (75), 23-Окт-26, 13:51
	По-вашему, реализации архитектуры RISC-V написаны на святам духе? Они также написаны на HDL: Verilog, Chisel.
	Ответить | Правка | К родителю #17 | Наверх | Cообщить модератору

	93. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:59
	Нет, но есть железо без существующих дырявых концепций, как предсказание ветвлений и кеш
	Ответить | Правка | Наверх | Cообщить модератору

	104. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (39), 23-Окт-26, 14:52
	Ага, микроконтроллеры всякие.
	Ответить | Правка | Наверх | Cообщить модератору

	105. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 15:07
	В riscv есть on chip sram, гораздо лучше чем кеш, если уметь программировать. Кожаным это не дано, ИИ с этим справится легко.
	Ответить | Правка | Наверх | Cообщить модератору

	106. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 15:07
	рассмешил, открой армовый М профиль и посмотри сколько UB в его ISA.
	Ответить | Правка | К родителю #104 | Наверх | Cообщить модератору

	142. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 18:21
	Не сравнивал жопу с пальцем, arm и riscv
	Ответить | Правка | Наверх | Cообщить модератору

	152. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 19:15
	подробней
	Ответить | Правка | Наверх | Cообщить модератору

	168. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (168), 23-Окт-26, 20:15
	ARM как первый все грабли собрал и у них нет настраиваемого ISA. Базовую реализацию RiscV RV32IM уже можно саму верифицировать и код исполняющейся на ней тоже. И есть реальные железки которые только это умеют.
	Ответить | Правка | Наверх | Cообщить модератору

	114. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (75), 23-Окт-26, 15:37
	Да даже без если кеша вообще и без спекулятива, всё равно, проектируюься на HDL. Не думаете же ли вы, что топологию на куче ватманов расчерчивают
	Ответить | Правка | К родителю #93 | Наверх | Cообщить модератору

	170. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (168), 23-Окт-26, 20:17
	Так ее саму можно верифицировать без особых проблем
	Ответить | Правка | Наверх | Cообщить модератору

	150. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 18:56
	> Начать надо с верификации верилога процессора. А то окажется что там напортачили > со спекулятивным исполнением инструкций 🤷♂ Так ты токены не продашь хомякам
	Ответить | Правка | К родителю #15 | Наверх | Cообщить модератору

	19. "Аnthropic развивает технику для формальной верификации сущес..."	–3 +/–
	Сообщение от Аноним (19), 23-Окт-26, 11:22
	Кожаные гении, посчитайте, сколько UB в этом ванильном и типичном коде самого популярного языка на планете: int sum; for (int i = 0; i <= INT_MAX; i++)     sum += 2;
	Ответить | Правка | К родителю #9 | Наверх | Cообщить модератору

	23. "Аnthropic развивает технику для формальной верификации сущес..."	+3 +/–
	Сообщение от Bottle (?), 23-Окт-26, 11:34
	1. Неявно задана сумма. 2. Когда индекс станет инт_макс, будет знаковое переполнение. 3. Сумма к тому моменту будет знаково переполнена дважды? Нет уверенности из-за первого неопределённого поведения.
	Ответить | Правка | Наверх | Cообщить модератору

	54. "Аnthropic развивает технику для формальной верификации сущес..."	–2 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:08
	Вот, а это типичный код, которого миллионы строк на github. Обученный ИИ до такого никогда не додумается
	Ответить | Правка | Наверх | Cообщить модератору

	65. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Смузихеб забывший пароль (?), 23-Окт-26, 13:21
	едва ли это типичный код вдобавок, а на каком коде, думаешь, этот ИИ обучают ?)
	Ответить | Правка | Наверх | Cообщить модератору

	71. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:33
	Надеюсь, что не на таком. Или такой используют для контрпримеров
	Ответить | Правка | Наверх | Cообщить модератору

	78. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (82), 23-Окт-26, 13:41
	> Надеюсь, что не на таком. Или такой используют для контрпримеров Забавный вы. И очень наивный.
	Ответить | Правка | Наверх | Cообщить модератору

	91. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:57
	Расскажи как проходит обучение трансформера языку программирования, а мы послушаем
	Ответить | Правка | Наверх | Cообщить модератору

	96. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (82), 23-Окт-26, 14:01
	Что такое "трансформер"?
	Ответить | Правка | Наверх | Cообщить модератору

	98. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (10), 23-Окт-26, 14:14
	Понял, вопросов больше не имею
	Ответить | Правка | Наверх | Cообщить модератору

	110. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (82), 23-Окт-26, 15:17
	> Понял, вопросов больше не имею Ответ на реплику выше. трансформер — это удачный маркетинговый бренд Реально это - архитектура сквозного внимания или нейросети с механизмом самовнимания. Термин трансформер создает иллюзию, что все эти модели условной серии GPT устроены одинаково. На самом деле архитектура состояла из двух половин — энкодера и декодера. Сегодня их пути разошлись: BERT — это чистый энкодер GPT / Claude / Gemini — это чистые авторегрессионные декодеры Ну и так далее... там еще 4 пункта проблем этого термина.
	Ответить | Правка | К родителю #96 | Наверх | Cообщить модератору

	86. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (86), 23-Окт-26, 13:47
	А на каком его ещё обучать, если другого нет? В php или linux дыры от хорошей жизни завелись?
	Ответить | Правка | К родителю #65 | Наверх | Cообщить модератору

	95. "Аnthropic развивает технику для формальной верификации сущес..."	–2 +/–
	Сообщение от Аноним (10), 23-Окт-26, 14:01
	Тем дырам сто лет в обед, когда ещё на слуху были только экспертные системы в медицине. ИИ просто их нашла
	Ответить | Правка | Наверх | Cообщить модератору

	127. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (86), 23-Окт-26, 16:30
	По вашей логике сейчас в php и linux должно быть ровно 0 дыр. Если есть хотя бы одна дыра, то её опять проглядели.
	Ответить | Правка | Наверх | Cообщить модератору

	29. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (29), 23-Окт-26, 11:48
	Слишком просто. Попробуйте ещё раз.
	Ответить | Правка | К родителю #19 | Наверх | Cообщить модератору

	100. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (100), 23-Окт-26, 14:27
	Даже впадлу такой бред разбирать, тут и переполнение и использование неинициализированной переменной. А бред потому что покажи пример этого "типичного" кода в опенсорсе. Можно прям ссылкой на номер строки в гитхабе.
	Ответить | Правка | К родителю #19 | Наверх | Cообщить модератору

	112. "Аnthropic развивает технику для формальной верификации сущес..."	–12 +/–
	Сообщение от Аноним (10), 23-Окт-26, 15:26
	Да без проблем. Тыкнул в случайный файл DPDK, который кстати в другой новости обсуждается. И что мы видим? static void graph_insert_ordered(struct graph *graph) {     struct graph *after, *g;     after = NULL;     STAILQ_FOREACH(g, &graph_list, next) {         if (g->id < graph->id)             after = g;         else if (g->id > graph->id)             break;     }     if (after == NULL) {         STAILQ_INSERT_HEAD(&graph_list, graph, next);     } else {         STAILQ_INSERT_AFTER(&graph_list, after, graph, next);     } } Переменная after инициализируется в первом цикле только в одной ветке. И следующая проверка if (after == NULL) что нам скажет, если сишники принципиально не инициализирует свои переменные при объявлении? И это код который используется в датацентрах и финтехе, Карл!
	Ответить | Правка | Наверх | Cообщить модератору

	116. "Аnthropic развивает технику для формальной верификации сущес..."	+3 +/–
	Сообщение от черпало (?), 23-Окт-26, 15:41
	Ты дебил или троллишь? Кекспертиза как всегда. after = NULL прямо перед форычем, ты внатуре такой дебил? Почему, почему именно такие персоны и орут больше всех? Боже, за что всё это
	Ответить | Правка | Наверх | Cообщить модератору

	117. "Аnthropic развивает технику для формальной верификации сущес..."	–7 +/–
	Сообщение от Аноним (10), 23-Окт-26, 15:54
	Вот видишь, человек проглядел инициализацию. Так же может проглядеть и наоборот. А вот rust не проглядел бы. Да и ИИ находит кучу того, что проглядели кожаные.
	Ответить | Правка | Наверх | Cообщить модератору

	134. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
	Сообщение от черпало (?), 23-Окт-26, 17:56
	Обгадился, но рационализируешь? У тебя во всей теме сообщения, которые показывают твой уровень. Такому не помогут ни ии, ни раст, ни лысый чёрт, только букварем по затылку охаживать. Ты не в состоянии понять простые вещи, а бросаешься рассуждать о вещах чуть сложнее. Еще и с ненавистью и неприязнью к другим инструментам. Это буквально позорище, и именно такие персоны составляют ядро верунов в раст и волшебныйй ии (конешно, ведь это автоматически происходит: перчатки надел -- боксёр, в самолет сел -- пилот). Ты буквально от натуги лопнешь (еще и с апломбом будешь чушь нести), не видя границы своего понимания сущего. Тьфу
	Ответить | Правка | Наверх | Cообщить модератору

	135. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 17:59
	Это не то что статический анализатор находит, это компилятор сишный обычный увидит и предупредит, а с -Вэррор еще и откажется такой гумусный код компилить.
	Ответить | Правка | К родителю #117 | Наверх | Cообщить модератору

	221. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (100), 24-Окт-26, 09:06
	> Переменная after инициализируется в первом цикле только в одной ветке. И следующая проверка if (after == NULL) что нам скажет, если сишники принципиально не инициализирует свои переменные при объявлении? Скажет что всё ок - переменная инициализированна сразу после объявления. > И это код который используется в датацентрах и финтехе, Карл! И что? Нормальный же код.
	Ответить | Правка | К родителю #112 | Наверх | Cообщить модератору

	151. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 18:56
	> Кожаные гении, посчитайте, сколько UB в этом ванильном и типичном коде самого > популярного языка на планете: > int sum; > for (int i = 0; i <= INT_MAX; i++) >     sum += 2; Справедливости ради современные компиляторы выдадут предупреждение и ИИ выдаст тебе проблемы этого кода, если попросить.
	Ответить | Правка | К родителю #19 | Наверх | Cообщить модератору

	153. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 19:17
	> Справедливости ради если кому-то нужно в этом коде искать проблемы аж с помощью ии, то ставлю коньяк, что этот спесалист ложку к уху несет, слюни у него капают, в речи отмечаются слова "раст", "дырени", и проч, вид имеет очень важный и напыщенный. кажется, когда эти спесалисты были ростом меньше метра, компиляторы это умели. Действительно кто-то думает, что с ии эти персонажи СМОГУТ?
	Ответить | Правка | Наверх | Cообщить модератору

	155. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 19:31
	>> Справедливости ради > если кому-то нужно в этом коде искать проблемы аж с помощью ии, > то ставлю коньяк, что этот спесалист ложку к уху несет, слюни > у него капают, в речи отмечаются слова "раст", "дырени", и проч, > вид имеет очень важный и напыщенный. > кажется, когда эти спесалисты были ростом меньше метра, компиляторы это умели. > Действительно кто-то думает, что с ии эти персонажи СМОГУТ? По факту это косяки языка и они есть. В расте их нет, по крайней мере выше перечисленных. Пробелма в том, что они могут вылезти в других ситуациях, примеров переполнений полно в cve.
	Ответить | Правка | Наверх | Cообщить модератору

	159. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 19:58
	По какому факту какие косяки? опиши прям по пунктам. И я задал вопрос, давай повторю: если для анализа двух таких строчек болванчику нужен ии и раст (и болванчик не знает о флагах компилятора), то этот самый болванчик сможет ли что дельное сотворить (или проверить, что ии ему выдал)? Может такой болванчик вступать в дискуссии на каком-то разумном уровне и демонстрировать понимание в принципе? Отсутствие принудительной инициализации -- это косяк, по-твоему? Есть флаг и для такого, кстати, нулями забивать или каким poison. Ворнинг будет всегда, его можно и в ошибку превратить. Догадаешься, почему по умолчанию так не сделано? Целочисленное переполнение? Ну, щас бы для каждой архитектуры описывать, что там получиться должно. Почитай, в конце-концов, Rationale, почему так сделано. Освободили транслятор от работы, переложили работу на программера (вот где проблема). Или тебе отдельно про алгебру и оптимизации лекцию провести (это вторая причина)? Нет уж, иди сам читай. Веб-синьоры до увлечения растом не знали никаких слов о типах данных, а щас выучили (но только слова). Можно, конечно, добавить smt-прувер для интов в компилер, но зачем? Да и зачем высокоуровневый очень наглядный асм обвешивать мишурой, не понимаю. Сишка тащит груз совместимости, простоты и кучу другого груза еще с мейнфреймовых времен, и удачно, надо сказать. И там явно сказано, что все проблемы от программиста, это все его зона ответственности -- все проверки. И тут приходит (двадцать лет назад, бгг, и сразу устаревший) язык, на который налипают одичавшие веб-синьоры, которые вдруг почувствовали какую-то силу. И каждый раз, вступая в дискуссии и пытаясь полировать свой любимый инструмент, охаивая другой, закономерно садятся в лужу.
	Ответить | Правка | Наверх | Cообщить модератору

	166. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 20:12
	> По какому факту какие косяки? опиши прям по пунктам. > Отсутствие принудительной инициализации -- это косяк, по-твоему? Есть флаг и для такого, > кстати, нулями забивать или каким poison. > Ворнинг будет всегда, его можно и в ошибку превратить. Догадаешься, почему по > умолчанию так не сделано? Косяк в том, что компилятор дает возможность использовать такую переменную в отличие от раста. Флаги не все ловят не все кейсы, зависят от компилятора, в рантайме ловит только memory sanitizer, которого в gcc нет. > Целочисленное переполнение? Ну, щас бы для каждой архитектуры описывать, что там получиться > должно. Почитай, в конце-концов, Rationale, почему так сделано. Освободили транслятор > от работы, переложили работу на программера (вот где проблема). Или тебе > отдельно про алгебру и оптимизации лекцию провести (это вторая причина)? Нет > уж, иди сам читай. Проблема была в архитектурах, которые уже не актуальны. Более того Начиная со стандарта C++20, язык официально зафиксировал, что все знаковые целые числа (signed integers) обязаны храниться в дополнительном коде (two's complement). Раньше стандарт допускал и другие варианты (например, прямой код или обратный код). А еще в с23 добавили checked arithmetic. Зачем, если и так все ок? > Можно, конечно, добавить smt-прувер для интов в компилер, но зачем? Да и > зачем высокоуровневый очень наглядный асм обвешивать мишурой, не понимаю. > Сишка тащит груз совместимости, простоты и кучу другого груза еще с мейнфреймовых > времен, и удачно, надо сказать. И там явно сказано, что все > проблемы от программиста, это все его зона ответственности -- все проверки. SMT-прувер, который будет по таймауту отваливаться и для которого ты будешь леммы писать на rocq? Ты думаешь достаточно умных слов сказать и все? Ну покажи мне свои прувы на ACSL.
	Ответить | Правка | Наверх | Cообщить модератору

	172. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 20:21
	> Косяк в том, что компилятор дает возможность использовать такую переменную в отличие > от раста. Молча дает? Вот прям молчит? Штош. > Проблема была в архитектурах, которые уже не актуальны. Более того > Начиная со стандарта C++20, язык официально зафиксировал, что все знаковые целые числа > (signed integers) обязаны храниться в дополнительном коде (two's complement). Раньше стандарт > допускал и другие варианты (например, прямой код или обратный код). Ты мне что-то новое открыл или я сказал не то же самое? Ты только что это нагуглил или текст мой не понял? > А еще в с23 добавили checked arithmetic. Зачем, если и так все > ок? кто и когда сказал, что ок? Ты лично читал Rationale? > SMT-прувер, который будет по таймауту отваливаться и для которого ты будешь леммы > писать на rocq? Ты думаешь достаточно умных слов сказать и все? > Ну покажи мне свои прувы на ACSL. ты не одупляешь иронии или читаешь плохо? я сказал, что "можно, но зачем" добавлять к высокоуровневому ассемблеру прувер. Я думаю, шо раз я прикручивал сам через плагин компиляторный прувер, то могу говорить об этом. прикинь, рефайнед типы в высокоуровневом асме! придите и поклонитесь!
	Ответить | Правка | Наверх | Cообщить модератору

	175. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 20:39
	>> Косяк в том, что компилятор дает возможность использовать такую переменную в отличие >> от раста. > Молча дает? Вот прям молчит? Штош. https://godbolt.org/z/xxejsbzr7 #include <iostream> class Foo { public:     Foo() {         init();     } private:     void init() {         std::cout << x << "\n";     }     int x; }; int main() {     Foo(); } $ g++ -std=c++23 -Wall -Werror -Wpedantic main.cpp $ ./a.out 29212 >> Проблема была в архитектурах, которые уже не актуальны. Более того >> Начиная со стандарта C++20, язык официально зафиксировал, что все знаковые целые числа >> (signed integers) обязаны храниться в дополнительном коде (two's complement). Раньше стандарт >> допускал и другие варианты (например, прямой код или обратный код). > Ты мне что-то новое открыл или я сказал не то же самое? > Ты только что это нагуглил или текст мой не понял? Ты же защищаешь это поведение, а от него отказываются.
	Ответить | Правка | Наверх | Cообщить модератору

	178. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 21:25
	> Ты же защищаешь это поведение, а от него отказываются. Я защищаю задокументированное поведение от крикунов-растовиков (ну как, скорее посмеиваюсь). То, что буквально написано буквами "за всё отвечает программист". Проблема не в инструменте. Да и не в программерах, которые на авось пишут. Историю, корнями проросшую везде. Факт, что нельзя выкинуть вообще все. То, что ну не могут те, кто в двух соснах путается, написать ни с ии, ни с растом ничего дельного, как бы не орали они. Может, покажешь, где я говорил "это всё хорошо"? Я сторонник исправлять и улучшать то, что есть. Сторонник не слепо верить в серебряные пули и сверхвозможности без всяких оснований. Говорю, что у такого поведения есть причины (в том числе и исторические). А по поводу твоего кода, я даже объяснить могу, почему так происходит, про ИПА, про правила анализа и правила крестов, но очень уж уныло, чел. Да и вертел я их, кресты-то (хотел бы я в прошлое, шоб и их не видеть, и страуструпу бабу найти или на мет подсадить). Вот, добавил один ключик к твоим, ииииии... <source>: In constructor 'Foo::Foo()': <source>:5:5: warning: 'Foo::x' should be initialized in the member initialization list     5 |     Foo() {       |     ^~~ ASM generation compiler returned: 0 <source>: In constructor 'Foo::Foo()': <source>:5:5: warning: 'Foo::x' should be initialized in the member initialization list     5 |     Foo() {       |     ^~~ Execution build compiler returned: 0 Program returned: 0 32765
	Ответить | Правка | Наверх | Cообщить модератору

	183. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:22
	>[оверквотинг удален] >     5 |     Foo() { >       |     ^~~ > ASM generation compiler returned: 0 > <source>: In constructor 'Foo::Foo()': > <source>:5:5: warning: 'Foo::x' should be initialized in the member initialization list >     5 |     Foo() { >       |     ^~~ > Execution build compiler returned: 0 > Program returned: 0 > 32765 Какой ключик ты добавил? Дай ссылку на godbolt
	Ответить | Правка | Наверх | Cообщить модератору

	184. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:32
	>> Ты же защищаешь это поведение, а от него отказываются. > То, что буквально написано буквами "за всё отвечает программист". Проблема не в > инструменте. > Да и не в программерах, которые на авось пишут. Вот это ошибочно на мой взгляд. Компилятор - это инструмент и чем больше он скажет, тем лучше. Сейчас вот начали добавлять предупреждений разных. Разве нормально, что ошибка в строке формата приводит к cve?
	Ответить | Правка | К родителю #178 | Наверх | Cообщить модератору

	203. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 23:55
	> <source>:5:5: warning: 'Foo::x' should be initialized in the member initialization list Слишком сильное ограничение. А в расте такое по умолчанию. Вотъ!
	Ответить | Правка | К родителю #178 | Наверх | Cообщить модератору

	157. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 19:37
	>> Справедливости ради > если кому-то нужно в этом коде искать проблемы аж с помощью ии, > то ставлю коньяк, что этот спесалист ложку к уху несет, слюни > у него капают, в речи отмечаются слова "раст", "дырени", и проч, > вид имеет очень важный и напыщенный. Другой вопрос: почему простой цикл таит в себе столько проблем? Потом удивляемся почему раст предпочитают с++. Конечно, когда ты с большим опытом, то для тебя кажтеся это очевидным, ведь ты уже прошел 10 раз по граблям и набил шишек. Вот только даже у таких код , собранный с fsanitize падает, а в проде cve. И внезапно компиляторы стали анализировать и давать ворнинги, хотя раньше ub была "фишкой".
	Ответить | Правка | К родителю #153 | Наверх | Cообщить модератору

	163. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 23-Окт-26, 20:04
	ты пьяный, что ли? где и в каких племенах UB было "фишкой"? Это способ генерировать и оптимизировать код по все доступные архитектуры, переложив всё на программера. Необходимое зло, так сказать. Опасное, жуть. Но, скажи мне, почему вдруг вылупились создания, которые считают, что можно нажуевертить чего угодно, не читая и не понимая матчасть? Проблема не в расте, а в его полоумных фанатах. Почему у этих созданий в голове не укладывается, что полувековая история языка -- это штука несколько более сложная, чем "да щас выкинем и перепишем"?
	Ответить | Правка | Наверх | Cообщить модератору

	169. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 20:17
	> ты пьяный, что ли? где и в каких племенах UB было "фишкой"? > Это способ генерировать и оптимизировать код по все доступные архитектуры, переложив всё > на программера. > Необходимое зло, так сказать. > Опасное, жуть. Тебе раст сгенерит аналогичный по производительности код, выявив на этапе компиляции проблемы. > Но, скажи мне, почему вдруг вылупились создания, которые считают, что можно нажуевертить > чего угодно, не читая и не понимая матчасть? Проблема не в > расте, а в его полоумных фанатах. Мы не об этом сейчас. Если инструмент позволяет выявить проблемы, то порог входа снижается. Это же хорошо с одной стороны. Сейчас вот есть разные ЧПУ домашние станки и софт, можешь делать разное, моделировать, при этом не вдаваясь особо сильно в матчасть.
	Ответить | Правка | Наверх | Cообщить модератору

	171. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 20:19
	> ты пьяный, что ли? где и в каких племенах UB было "фишкой"? > Это способ генерировать и оптимизировать код по все доступные архитектуры, переложив всё > на программера. Вот сишники как раз это и приподносили как "фишку" и сейчас преподносят. Только вот поток cve только повысился и ИИ находит в их "необходимом" зле реальное зло.
	Ответить | Правка | К родителю #163 | Наверх | Cообщить модератору

	179. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 21:36
	> Вот сишники как раз это и приподносили как "фишку" и сейчас преподносят. Не "сишники", а компиляторостроители. И не UB как фишку, а как необходимость канпелять и применять правила алгебраические. Это _обоснованно_. Это данность. Хорошо ли? Ну как сказать. с checked arithmetic такого не сделать, да и для другого это вот. > Только вот поток cve только повысился и ИИ находит в их > "необходимом" зле реальное зло. Так потому что инструменты улучшаются, и это хорошо. Берем эти инструменты, отправляемся в прошлое, никаких CVE нет. ВУА-ЛЯ! СИЛЬ-ВУ-ПЛЕ!
	Ответить | Правка | Наверх | Cообщить модератору

	188. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:47
	>> Вот сишники как раз это и приподносили как "фишку" и сейчас преподносят. > Не "сишники", а компиляторостроители. И не UB как фишку, а как необходимость > канпелять и применять правила алгебраические. Это _обоснованно_. Это данность. > Хорошо ли? Ну как сказать. > с checked arithmetic такого не сделать, да и для другого это вот. Все еще жду от тебя архитектуру на сегодняшний день, ради которой надо смиряться с UB. В частности с невозможносью wrap-around для singed int. > Так потому что инструменты улучшаются, и это хорошо. > Берем эти инструменты, отправляемся в прошлое, никаких CVE нет. ВУА-ЛЯ! СИЛЬ-ВУ-ПЛЕ! Они есть, просто их не нашли.
	Ответить | Правка | Наверх | Cообщить модератору

	181. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (181), 23-Окт-26, 22:15
	> Это способ генерировать и оптимизировать код по все доступные архитектуры, переложив всё на программера. > Необходимое зло, так сказать. Да конечно. Сишка делалась про конкретную архитектуру.
	Ответить | Правка | К родителю #163 | Наверх | Cообщить модератору

	189. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 22:49
	Всю тыщщу лет, или сначала хотели наполши^W для одной, а потом понеслось, и пришлось чот какое-то UB для дыреней?
	Ответить | Правка | Наверх | Cообщить модератору

	167. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 23-Окт-26, 20:14
	Я определённо точно могу тебе описать и рассказать с примерами (от разных архитектур, асма и алгебры), почему "простой" (нет) цикл "таит" (нет) в себе столько "проблем" (нет). Компухтер сайнс -- нон пенис канина. Ты мне скажи, программист, откуда пошло предположение, что к циркулярной пиле нужно детей допускать? бггг, смеюсь конешно. скажи, bool test = x + 1 > x -- это UB или нет, и почему?
	Ответить | Правка | К родителю #157 | Наверх | Cообщить модератору

	174. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 20:26
	> скажи, bool test = x + 1 > x -- это UB > или нет, и почему? От типа x зависит. Если знаковое целое, то может быть. В том и дело, что любой + потенциальное уб в зависимости от значения без доп. флагов. Но раст вот далает панику в дебаге и wraparound в релизе, что лучше чем уб, конечно же. Назови мне лучше архитектуры, на которых бы это приводило к неоптимальному коду на сегодняшний день?
	Ответить | Правка | Наверх | Cообщить модератору

	176. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 21:02
	> В том и дело, что любой + потенциальное уб в зависимости от значения > без доп. флагов. Нет, не любой, а небольшое подмножество +, еще и от типа аккумулятора зависит. Черт ногу сломит, но правила есть. И нет, не "может быть". По той же причине (x * 2) / 2 -- не UB. Если везде вкорячивать проверки, никакой оптимизации по правилам алгебры быть не может. Покажи мне компилятор, вот с того же годболта, который не упростит  x + 1 > x до mov eax, 1
	Ответить | Правка | Наверх | Cообщить модератору

	182. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:19
	>> В том и дело, что любой + потенциальное уб в зависимости от значения >> без доп. флагов. > Нет, не любой, а небольшое подмножество + Что значит небольшое поднможество? У тебя опреатор + определен на множестве целых числе со знаком. Если ты сложил signed int и получил переполнение, то это уб. > И нет, не "может быть". По той же причине (x * 2) > / 2 -- не UB. Если везде вкорячивать проверки, никакой оптимизации > по правилам алгебры быть не может. Достаточно не делать уб по стандарту. В расте лучше сделано на мой взгляд. > Покажи мне компилятор, вот с того же годболта, который не упростит   > x + 1 > x до mov eax, 1 https://godbolt.org/z/87nzT5Pv8 ```rust #![feature(unchecked_math)] use std::hint::black_box; #[unsafe(no_mangle)] pub unsafe fn test_unchecked(x: i32) -> bool {     x.unchecked_add(1) > x } pub fn main() {     let input = black_box(42);     let res = unsafe { test_unchecked(input) };     println!("{}", res); } ``` ```asm test_unchecked:         mov     al, 1         ret ```
	Ответить | Правка | Наверх | Cообщить модератору

	186. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 22:45
	> Что значит небольшое поднможество? У тебя опреатор + определен на множестве целых > числе со знаком. Если ты сложил signed int и получил переполнение, > то это уб. если я сложил два знаковых целых (по МАКС_ИНТ каждый) и положил результат в знаковое целое побольше -- все ок, не UB, все влезает. Правила такие. В стандарт тыкнуть или сам найдешь? "небольшое подмножество" значит, что не все + одинаково андефайнед. У каждого андефайнед есть причина и место. И да, нет просто "целых", тут тебе не матан, а железяки. >> И нет, не "может быть". По той же причине (x * 2) >> / 2 -- не UB. Если везде вкорячивать проверки, никакой оптимизации >> по правилам алгебры быть не может. > Достаточно не делать уб по стандарту. В расте лучше сделано на мой > взгляд. Я бы не строил компиляторы, основываясь на твоем взгляде. Уж извини, то, что ты весь разговор демонстрируешь, меня печалит. Ты, рассказывая про UB, не ответил про него правильно. Ну не ответил же. >> Покажи мне компилятор, вот с того же годболта, который не упростит >> x + 1 > x до mov eax, 1 > ```asm > test_unchecked: >         mov     >  al, 1 >         ret > ``` Бгг, бль, боже, чел. Какая невероятная жесть, боже. Аж больно стало. Ну да, ну да, не mov eax, 1, ага. а что там выше за волшебство? вот это вот mov byte ptr [rsp + 3], 1? Что за зверь такой на месте вызова, почему оно туда кладет константу? Почему не врапараундится, не паникует? Скажи, ты пьян?
	Ответить | Правка | Наверх | Cообщить модератору

	190. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:54
	>> Что значит небольшое поднможество? У тебя опреатор + определен на множестве целых >> числе со знаком. Если ты сложил signed int и получил переполнение, >> то это уб. > если я сложил два знаковых целых (по МАКС_ИНТ каждый) и положил результат > в знаковое целое побольше -- все ок, не UB, все влезает. > Правила такие. В стандарт тыкнуть или сам найдешь? Стоп-стоп. А причем тут promotion типов? Тип определяет множество значений, соответственно операция определена над типом. Ну давай скажем, что у тебя уже int64_t и дальше что? 128 бит? > "небольшое подмножество" значит, что не все + одинаково андефайнед. У каждого андефайнед > есть причина и место. И да, нет просто "целых", тут тебе > не матан, а железяки. Это софистика. Любой + может привести к уб. Все зависит от значений в знаковых целых. Это может произойти в любом месте программы. Поэтому компилятор тут тебе не особо помощник.
	Ответить | Правка | Наверх | Cообщить модератору

	196. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 23:16
	> Это софистика. Любой + может привести к уб. Все зависит от значений > в знаковых целых. Это может произойти в любом месте программы. Поэтому > компилятор тут тебе не особо помощник. Нет, дружок, кванторы всеобщности тут не работают, как бы тебе не хотелось нагнать паники. И тут помощник именно компилятор. И не тот, который заставляет области видимости прописывать, а поумней. Как бы то ни было, это все как раз дело компилятора.
	Ответить | Правка | Наверх | Cообщить модератору

	192. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 23:00
	> Почему не врапараундится, не паникует? Потому что явный unchecked и УБ. Все как ты любишь.
	Ответить | Правка | К родителю #186 | Наверх | Cообщить модератору

	195. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 23:07
	>> Почему не врапараундится, не паникует? > Потому что явный unchecked и УБ. Все как ты любишь. mov byte ptr [rsp + 3], 1? положить по указателю константу 1 -- это UB и аж анчекед? Как страшно жить.
	Ответить | Правка | Наверх | Cообщить модератору

	185. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:38
	>> В том и дело, что любой + потенциальное уб в зависимости от значения >> без доп. флагов. > Покажи мне компилятор, вот с того же годболта, который не упростит   > x + 1 > x до mov eax, 1 НЕ упростит? Ну safe версия будет такой (wrap-around): test_regular:         cmp     edi, 2147483647         setne   al         ret
	Ответить | Правка | К родителю #176 | Наверх | Cообщить модератору

	187. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 23-Окт-26, 22:46
	>>> В том и дело, что любой + потенциальное уб в зависимости от значения >>> без доп. флагов. >> Покажи мне компилятор, вот с того же годболта, который не упростит >> x + 1 > x до mov eax, 1 > НЕ упростит? Ну safe версия будет такой (wrap-around): > test_regular: >         cmp     >  edi, 2147483647 >         setne   al >         ret Бгг, то есть, математически корректный код скажет false при х == INT_MAX? кайф
	Ответить | Правка | Наверх | Cообщить модератору

	191. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 22:57
	>[оверквотинг удален] >>> Покажи мне компилятор, вот с того же годболта, который не упростит >>> x + 1 > x до mov eax, 1 >> НЕ упростит? Ну safe версия будет такой (wrap-around): >> test_regular: >>         cmp >>  edi, 2147483647 >>         setne   al >>         ret > Бгг, то есть, математически корректный код скажет false при х == INT_MAX? > кайф Ты сейчас прикидываешься? Произойдет wrap-around и, конечно, будет false. Но лучше, конечно, UB? Правда, сишник?
	Ответить | Правка | Наверх | Cообщить модератору

	194. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 23-Окт-26, 23:05
	Смотрю, дружок, ты недалеко уехал от растофанов. И это печально. А так начал :( И ключиком для крестов облом, и с пониманием. Читай внимательнее: Там. Нет. UB. Вообще. Совсем. В приведенных мною примерах нет UB. понимаешь? В приведенных примерах для Си нет этого, оно упрощается. Нет. Вообще нет. Потому что это математически корректная штука. Там не может быть UB. Давай еще раз, чтоб все видели: В расте выражения, эквивалентные для си, со знаковым целым х == INT_MAX, дадут неверный результат? 1) bool b = x + 1 > x 2) int i = (x * 2) / 2
	Ответить | Правка | Наверх | Cообщить модератору

	197. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 23:21
	> Смотрю, дружок, ты недалеко уехал от растофанов. И это печально. А так > начал :( > И ключиком для крестов облом, и с пониманием. > Читай внимательнее: > Там. Нет. UB. Вообще. Совсем. > В приведенных мною примерах нет UB. понимаешь? В приведенных примерах для Си > нет этого, оно упрощается. > Нет. Вообще нет. Потому что это математически корректная штука. Там не может > быть UB. Это бред. По стандарту оно есть. Компилятор просто вставляет true, потому что UB случаться не может по его мнению и тебе просто везет.
	Ответить | Правка | К родителю #194 | Наверх | Cообщить модератору

	199. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 23-Окт-26, 23:29
	Давай еще раз, чтоб все видели: В расте выражения, эквивалентные для си, со знаковым целым х == INT_MAX, дадут неверный результат? 1) bool b = x + 1 > x 2) int i = (x * 2) / 2 В последних предложениях ты почти понял, зачем UB вводилось (нет, не только архитектуры, но пэйперы сам почитай). Забрезжило понимание. Прям как деды завещали (и нет, мне не просто везет, мне просто оуеть как везет, чудо просто)
	Ответить | Правка | К родителю #197 | Наверх | Cообщить модератору

	204. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 24-Окт-26, 02:07
	> В последних предложениях ты почти понял, зачем UB вводилось Я и так знал зачем оно было нужно тогда. Зачем оно нужно сегодня пояснишь? Назови актуальную архитектуру из-за которой надо делать ub на сложение знаковых (4-ый раз уже тебя спрашиваю)?
	Ответить | Правка | К родителю #199 | Наверх | Cообщить модератору

	233. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 24-Окт-26, 13:57
	> Я и так знал зачем оно было нужно тогда. Нет, не знал (это же видно, бль, вот как у комментатора, из-за которого ветка началась), и даже не цитаты из гугла тебя выдают, а общее непонимание. Ты нагуглил, а смысла не понял. > Назови актуальную архитектуру из-за которой надо делать ub на > сложение знаковых (4-ый раз уже тебя спрашиваю)? Во-первых, перечитай ветку, я четко говорил n раз, что причина появления UB -- не только архитектуры, а еще и оптимизации, которые не были бы возможны, если везде пихать проверки (а они не везде нужны). Зачем предполагать, что в инт помещается бесконечность, ты сам показал, только, видимо, не понял ни примеров своих, ни нагугленной цитаты. И топать ножкой и требовать ответов -- шагай к производителям своим, либо для начала ответь на те вопросы мои, что без ответа остались. Начни с того, почему в расте положить константу 1 по указателю -- это UB, бггг. И да, очень показательный вышел разговор и показательная демонстрация раста (как и знатоков его) -- оно не может упростить выражение до тождественной истины и паникует, а это некорректно / может быть доказано. И "одинаково оптимальный код" -- смех один.
	Ответить | Правка | К родителю #204 | Наверх | Cообщить модератору

	237. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 24-Окт-26, 16:02
	>> Я и так знал зачем оно было нужно тогда. > Нет, не знал (это же видно, бль, вот как у комментатора, из-за > которого ветка началась), и даже не цитаты из гугла тебя выдают, > а общее непонимание. Ты нагуглил, а смысла не понял. Код, который ты приводишь содержит ub: https://en.cppreference.com/c/language/operator_arithmetic When signed integer arithmetic operation overflows (the result does not fit in the result type), the behavior is undefined: it may wrap around according to the rules of the representation (typically 2's complement), it may trap on some platforms or due to compiler options (e.g. -ftrapv in GCC and Clang), or may be completely optimized out by the compiler. Особенно перечитай вот это or may be completely optimized out by the compiler. Что собственно ты и наблюдаешь. То есть, ты сделал UB, наткнулся на поведение конкретного компилятора и пытаешься доказать, что это UB. >[оверквотинг удален] > Зачем предполагать, что в инт помещается бесконечность, ты сам показал, только, > видимо, не понял ни примеров своих, ни нагугленной цитаты. > И топать ножкой и требовать ответов -- шагай к производителям своим, либо > для начала ответь на те вопросы мои, что без ответа остались. > Начни с того, почему в расте положить константу 1 по указателю > -- это UB, бггг. > И да, очень показательный вышел разговор и показательная демонстрация раста (как и > знатоков его) -- оно не может упростить выражение до тождественной истины > и паникует, а это некорректно / может быть доказано. И "одинаково > оптимальный код" -- смех один. Ну вот собстенно, как и ожидал, ты не смог назвать актуальную архитектуру, ради которой все страдают от UB.
	Ответить | Правка | К родителю #233 | Наверх | Cообщить модератору

	238. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 24-Окт-26, 16:43
	> Давай еще раз, чтоб все видели: > В расте выражения, эквивалентные для си, со знаковым целым х == INT_MAX, > дадут неверный результат? > 1) bool b = x + 1 > x Что значит неверный результат? Инты конечны. Это не длинная арифметика. В расте будет false из-за wrap-around. В си это UB, может быть по разному в зависимости от компилятора https://en.cppreference.com/c/language/operator_arithmetic When signed integer arithmetic operation overflows (the result does not fit in the result type), the behavior is undefined: it may wrap around according to the rules of the representation (typically 2's complement), it may trap on some platforms or due to compiler options (e.g. -ftrapv in GCC and Clang), or may be completely optimized out by the compiler. Пример: $ cat t.c #include <stdio.h> #include <stdbool.h> #include <limits.h> int main(void) {     int x = INT_MAX;     bool r = x + 1 > x;     printf("%d\n", r);     return 0; } $ gcc t.c $ ./a.out 1 $ clang t.c $ ./a.out 0 $ cproc t.c $ ./a.out 0 Ссылки на godbolt gcc https://godbolt.org/z/6crf8xe6z clang https://godbolt.org/z/vTdr91nx3
	Ответить | Правка | К родителю #199 | Наверх | Cообщить модератору

	239. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 24-Окт-26, 18:03
	Да уж, чем дальше, тем очевиднее. Дружок, ты опять нагуглил что-то, что ты не понимаешь. Разница вывода и разница компиляторов тут не в обработке UB (в выражении нет UB). Тут разница в выхлопе из-за разницы проходов. Два последних компилятора тупые, они рано сворачивают константы, гцц умнее, он сворачивает предикат в тождественную истину. Тут о стандарте речи не идет, как и о неопределенном поведении. Это происходит НЕ потому, что выражение является UB, а потому что компиляторы обрабатывают константные выражения на разных этапах -- это разница между абстрактным логическим доказательством гцц и преждевременной эяку^W арифметической подстановкой шланга. Они втупую считают это и подставляют значения вместо оптимизации предиката. Сделай неизвестным икс, и все станет одинаковым на всем множестве интов (именно потому што стандарт говорит "никакого UB быть не может", бгг, магия софистики). Ты считаешь, что "completely optimized out by the compiler" означает, что компилятор удалил код, потому что в коде UB. Оптимизатор вырезает операцию сравнения (во всех приведенных компиляторах) не потому, что она (операция) сломалась, а потому, что ее результат заранее известен. Вырезается мертвый код. Причем, ты заладил про архитектуру (хотя и нагуглил про кольцо, но смысла не понял). Так вот на любой, где инты не бесконечны. Так понятнее? Я прекрасно понимаю, что ты лопнешь, будешь нести какие-то странные примеры (не понимая сути), путать причину и следствие. Вон как ты с крестами пришел в разговор про си или вот с примерами этими, но да ладно. Так что давай ты останешься при своих, возьмешь флаг победителя и пойдешь дальше разносить любование иишкой и растом (попроси иишку поругать меня, а то сам не справляешься. Или попроси объяснить тебе то, что ты на цппреференсе читаешь)
	Ответить | Правка | К родителю #238 | Наверх | Cообщить модератору

	241. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 24-Окт-26, 18:57
	>[оверквотинг удален] > Тут разница в выхлопе из-за разницы проходов. Два последних компилятора тупые, они > рано сворачивают константы, гцц умнее, он сворачивает предикат в тождественную истину. > Тут о стандарте речи не идет, как и о неопределенном поведении. > Это происходит НЕ потому, что выражение является UB, а потому что компиляторы > обрабатывают константные выражения на разных этапах -- это разница между абстрактным > логическим доказательством гцц и преждевременной эяку^W арифметической подстановкой > шланга. > Они втупую считают это и подставляют значения вместо оптимизации предиката. Сделай неизвестным > икс, и все станет одинаковым на всем множестве интов (именно потому > што стандарт говорит "никакого UB быть не может", бгг, магия софистики). Если бы это было так, то это нарушение стандарта и ты можешь смело заводить баг в clang. Но это не так. Выражение явный UB. Вот банально тоже самое в constexpr контексте, где UB запрещены: https://godbolt.org/z/ssoYbsW9K #include <cstdio> #include <climits> constexpr bool f() {     constexpr int x = INT_MAX;     return x + 1 > x; } int main() {     constexpr bool x = f();     return 0; } Соответственно получаем не 1 (или true), а ошибку компиляции error: overflow in constant expression [-fpermissive]     6 |     return x + 1 > x;       |            ~~^~~ Compiler returned: 1 > Ты считаешь, что "completely optimized out by the compiler" означает, что компилятор > удалил код, потому что в коде UB. > Оптимизатор вырезает операцию сравнения (во всех приведенных компиляторах) не потому, > что она (операция) сломалась, а потому, что ее результат заранее известен. > Вырезается мертвый код. Он не мертвый. Его результат используется. То, что код сворачивется в константу, говорит о том, что компилятор смог это сделать.   > Причем, ты заладил про архитектуру (хотя и нагуглил про кольцо, но смысла > не понял). Так вот на любой, где инты не бесконечны. Так > понятнее? Потому что ты не можешь привести пример реальной на сегодня используемой архитектуры. Соответственно не можешь и сказать на кой тащить этот UB сегодня? Оптимизации для каких архитектур? И если ты не заметил, то в новых стандартах уже сказали, что есть только одно представление в two's complement. > Я прекрасно понимаю, что ты лопнешь, будешь нести какие-то странные примеры (не > понимая сути), путать причину и следствие. Вон как ты с крестами > пришел в разговор про си или вот с примерами этими, но > да ладно. > Так что давай ты останешься при своих, возьмешь флаг победителя и пойдешь > дальше разносить любование иишкой и растом (попроси иишку поругать меня, а > то сам не справляешься. Или попроси объяснить тебе то, что ты > на цппреференсе читаешь) Ну нет. Давай ты приведешь пруфы для своих доводов. Докажи, что это не UB.
	Ответить | Правка | К родителю #239 | Наверх | Cообщить модератору

	245. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от черпало (?), 24-Окт-26, 20:09
	Ты продолжаешь бравировать глупостью, продолжаешь нести примеры, которые ты не понимаешь, продолжаешь путаться в терминологии. Прежде, чем нагугленное вываливать, потрудись понять или спросить нейронку. Ты не отличаешь операцию от выражения ведь. Ты не видишь разницы в проходах компилятора, и опять причину и следствие путаешь, балбес. Ты игнорируешь всё, что тебе говорят, но требуешь ответов? Богоизбранный гений, не иначе. Я сказал тебе убрать _вычисление_ с константой, что ты сделал вместо этого? принес мне пошаговое вычисление с константой в крестах? Ты упоролся? >> Вырезается мертвый код. > Он не мертвый. Его результат используется. То, что код сворачивется в константу, говорит о том, что компилятор смог это сделать.   Подучи терминологию. Это операции, вычисление которых в рантайме не требуется, так как их результат известен заранее. Результат используется, код сравнения — мертв, вырезан, потому что результат равен константе 1. Выражение не UB, потому что это СРАВНЕНИЕ, ты совсем не одупляешь, что ли? Допущение, что нет UB, позволяет свернуть это в 1. Вне зависимости от значений, это сворачивается в mov dst 1 Ты утомляешь своей глупостью, и даже не пытаешься понять, что тебе говорят, такая ригидность -- это просто полный вперёд. > Соответственно не можешь и сказать на кой тащить этот UB сегодня? Оптимизации для каких архитектур? И если ты не заметил, то в новых стандартах уже сказали, что есть только одно представление в two's complement. Вообще плевать на two's complement, ты читай, что тебе пишут, может, новое что узнаешь. Или гугли свои вопросы, сколько ж можно. Я тебе много раз написал, что дело не только в архитектурах (которые могут траповать и тд), дело в оптимизациях в том числе. Ты настолько непробиваемо деревянный, что я хз, куда тебя отправить. Представление инта как чисто математического объекта дает возможности векторизации, например, или вот такие инварианты считать. Вне зависимости от значений. Я тебя отсылал уже читать Rationale, раздел об оптимизациях на основе допущений. И да, я вижу, что ты не понимаешь разницы между крестами и си (ага, и стандарт один и тот же), продолжаешь упорствовать. Дело твое.
	Ответить | Правка | К родителю #241 | Наверх | Cообщить модератору

	158. "Аnthropic развивает технику для формальной верификации сущес..."	–10 +/–
	Сообщение от Аноним (158), 23-Окт-26, 19:53
	> если кому-то нужно в этом коде искать проблемы аж с помощью ии, Ты про разработчиков ядра? Громкое заявление) > то ставлю коньяк, что этот спесалист ложку к уху несет, слюни у него капают, в речи отмечаются слова "раст", "дырени", и проч, вид имеет очень важный и напыщенный. Угу, то ли дело СИшники, они выше всяких ИИ. Если обоcpaться - то по максимуму. Как с ПХП случилось. И с хартблидом. И с башдоором... > Действительно кто-то думает, что с ии эти персонажи СМОГУТ? Уже могут) В отличии от тех, кто с напыщенным видом очередную UBшку пишет.
	Ответить | Правка | К родителю #153 | Наверх | Cообщить модератору

	244. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 24-Окт-26, 19:30
	>> Справедливости ради > если кому-то нужно в этом коде искать проблемы аж с помощью ии, то ставлю коньяк Армяшка, ты ли это?
	Ответить | Правка | К родителю #153 | Наверх | Cообщить модератору

	80. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
	Сообщение от Аноним (100), 23-Окт-26, 13:43
	> когда на таких языках как C/C++ каждая вторая строчка это UB? Т.е. LLVM, который написан на C++, получается весь в UB? Это ж получается и раст компилится таким компилятором? Оу вей...
	Ответить | Правка | К родителю #9 | Наверх | Cообщить модератору

	89. "Аnthropic развивает технику для формальной верификации сущес..."	–4 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:55
	Прикинь, да... Нет ничего совершенного в этом мире. Алиасинг в LLVM чинили 10 лет, что бы он заработал как было спроектировано, а не как написано Васянами на C++.
	Ответить | Правка | Наверх | Cообщить модератору

	161. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Инопланетянин (?), 23-Окт-26, 20:00
	>> когда на таких языках как C/C++ каждая вторая строчка это UB? > Т.е. LLVM, который написан на C++, получается весь в UB? Это ж > получается и раст компилится таким компилятором? Оу вей... Не весь, до LLVM IR он на расте, в частности боров. Так что борова чекают без уб.
	Ответить | Правка | К родителю #80 | Наверх | Cообщить модератору

	11. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (29), 23-Окт-26, 11:05
	Воспроизводимость сборки и верификация кода - вещи разные, обе полезные.
	Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

	13. "Аnthropic развивает технику для формальной верификации сущес..."	–3 +/–
	Сообщение от Аноним (10), 23-Окт-26, 11:07
	Воспроизводимость сборки это тестирование компилятора. А зачем нужен компилятор когда ИИ умеет сразу в машинный код?
	Ответить | Правка | Наверх | Cообщить модератору

	27. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (29), 23-Окт-26, 11:47
	> Воспроизводимость сборки это тестирование компилятора. Нет. > А зачем нужен компилятор когда ИИ умеет сразу в машинный код? Тоже нет. Ещё вопросы?
	Ответить | Правка | Наверх | Cообщить модератору

	58. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:13
	Успешно прошел психологический курс - как научиться говорить нет?
	Ответить | Правка | Наверх | Cообщить модератору

	59. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:15
	Отвечу в стиле отладчика CP/M - ?
	Ответить | Правка | К родителю #27 | Наверх | Cообщить модератору

	108. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 15:11
	> А зачем нужен компилятор когда ИИ умеет сразу в машинный код? Компилятор ведь умнее человека, а значить и умнее ЫЫ :))
	Ответить | Правка | К родителю #13 | Наверх | Cообщить модератору

	32. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аныным (?), 23-Окт-26, 12:00
	Вопрос изначально некорректный, так исходный код описывает логику в рамках абстрактного исполнителя, оставляя кучу всего на откуп конкретного компилятора/интерпретатора. В случае анализа бинарников LLM просто статистическими методами пытается увидеть общую картину, но чаще всего это сложно, так как окно контекста забивается безумным объемом мелкозернистой логики.
	Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

	57. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:11
	Объемы логики это чисто техническая проблема, со временем научится обрабатывать все больше и больше
	Ответить | Правка | Наверх | Cообщить модератору

	109. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 15:13
	> так исходный код описывает логику в рамках абстрактного исполнителя рассмешил, ни один современный ЯП не описывает логику в рамках абстрактного исполнителя, а фактически повторяет своего исполнителя, тот же С, С++ и т.д.
	Ответить | Правка | К родителю #32 | Наверх | Cообщить модератору

	120. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 16:03
	А как же SQL?
	Ответить | Правка | Наверх | Cообщить модератору

	126. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (113), 23-Окт-26, 16:26
	Еще скажи HTML... точнее HTML + CSS, они же вместе тьюринг полные.
	Ответить | Правка | Наверх | Cообщить модератору

	132. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 17:31
	> Еще скажи HTML... точнее HTML + CSS, они же вместе тьюринг полные. да у него ведь бесконечная лента как у Тьюринга :)
	Ответить | Правка | Наверх | Cообщить модератору

	130. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 17:30
	> А как же SQL? давай, скомпилируй ка мне программу на несуществующей БД :)))
	Ответить | Правка | К родителю #120 | Наверх | Cообщить модератору

	33. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (86), 23-Окт-26, 12:01
	>тэк, огромадные специалисты в бям (больших языкастых моделях) БЯМ здесь не имеет абсолютно никакого отношения, речь исключительно о компиляции. >если бинарный файл собирается из одного исходника, но с разными параметрами оптимизации например, бям верифицирует конкретную сборку, или всё же логику исходного кода? БЯМ верифицирует один единственный файл. Если в процессе сборки что-то поменять, например заменить компилятор (gcc -> clang, gcc11 -> gcc12), любой флаг сборки -O0 -> -O2, то всё нужно начинать с нуля. Даже если бинарный патч наложить, то всё опять же с нуля.
	Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

	217. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (217), 24-Окт-26, 08:12
	В какой деревне LLM называют бям?
	Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

31. "Аnthropic развивает технику для формальной верификации сущес..."	+4 +/–
Сообщение от Аноним (86), 23-Окт-26, 11:57
>Ключевым преимуществом предложенного подхода является работа непосредственно с бинарными файлами, что позволяет обойтись без необходимости переписывания существующего кода на формально верифицируемых языках. Кому-то некуда деть деньги. Любая перекомпиляция и начинай всё с начала, с нуля.
Ответить | Правка | Наверх | Cообщить модератору

	69. "Аnthropic развивает технику для формальной верификации сущес..."	–2 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:31
	В этом суть экономики. Или ты продвигает принцип - экономика должна быть экономной?
	Ответить | Правка | Наверх | Cообщить модератору

38. "Аnthropic развивает технику для формальной верификации сущес..."	+3 +/–
Сообщение от Аноним (41), 23-Окт-26, 12:15
> на языке Rust был сгенерирован интерпретатор для подмножества языка Python > В 99.95% случаев результаты выполнения этих программ в новой реализации и в CPython совпали Тут сразу узнаётся разработка на безопасном языке, никогда не совпадающая по результату с оригиналом.
Ответить | Правка | Наверх | Cообщить модератору

	67. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:29
	Потому что в оригинале вместо логики - UB.
	Ответить | Правка | Наверх | Cообщить модератору

	74. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (82), 23-Окт-26, 13:37
	> Потому что в оригинале вместо логики - UB. Ты новости не читал? Там граничные случаи. На которые формальная верификация положила. От такого я аж прослезился. Верификация не проверяющая граничные случаи.... :)))
	Ответить | Правка | Наверх | Cообщить модератору

	77. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:40
	Ну ты так же ржал над первыми ИИ пару лет назад.
	Ответить | Правка | Наверх | Cообщить модератору

	123. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Xasd1 (?), 23-Окт-26, 16:15
	это был не он
	Ответить | Правка | Наверх | Cообщить модератору

	164. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (168), 23-Окт-26, 20:08
	Что не смеетесь? Не смешно? Не поняли, да? (C) Жириновский
	Ответить | Правка | Наверх | Cообщить модератору

	225. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (224), 24-Окт-26, 10:11
	> Ну ты так же ржал над первыми ИИ пару лет назад. Так ничего не поменялось. Оно делает выводы на аргументах, на которых такие выводы сделать нельзя. Тут только внешними инструментами править можно. Генетика не лечится.
	Ответить | Правка | К родителю #77 | Наверх | Cообщить модератору

63. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
Сообщение от Аноним (63), 23-Окт-26, 13:18
Уже выявили политические установки в весах китайских моделей - они допускают больше дыр для американских клиентов и существенно меньше для своих китайских. Ничто не мешает быть подобному и у антропиков. Поэтому флаг в руки и верьте всему что скажет ИИ
Ответить | Правка | Наверх | Cообщить модератору

	66. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:28
	Старо как мир, любое изобретение используется как оружие в первую очередь.
	Ответить | Правка | Наверх | Cообщить модератору

	76. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Смузихеб забывший пароль (?), 23-Окт-26, 13:38
	Это не просто "не мешает" Наверняка будет нечто вроде хмурых дядек из экспортного контроля( как было с амуде и его сотрудничеством по "китайскому процессору" ), которым потребуется именно фактически доказать и гарантировать, что эти наработки не ухудшат конкурентноспособность и положение на рынке американских компаний и не позволят зарубежным конторам получить преимущество перед ними Поэтому, в случае с той же амуде, китайцам, к примеру, достался лишь "выхлоп от исходников", где они могли менять параметры лишь одного блока( шифрование. На китайское ) и всё это на уже устаревшей архитектуре( т.е получался устаревший амд-проц с изменённым аппаратным шифрованием ) И это всё было полностью завязано на техпроцессы амд. В итоге, китайцы там что-то меняли, отправляли в амд, которая уже сама делала им кристаллы и после - отгружала в китай. От отправки в амд до получения кристаллов проходило неск мес - где-то полгода.
	Ответить | Правка | К родителю #63 | Наверх | Cообщить модератору

	85. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:47
	Поэтому российским разрабам сам бог велел использовать строгие языки, как rust, при использовании буржуйских ИИ
	Ответить | Правка | Наверх | Cообщить модератору

	208. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Боевой Петух (?), 24-Окт-26, 02:43
	Какой бред от профана.
	Ответить | Правка | К родителю #63 | Наверх | Cообщить модератору

	265. Скрыто модератором	+/–
	Сообщение от Аноним (-), 27-Окт-26, 10:07
	ну у нас тоже импортозамещение и национальный фокус
	Ответить | Правка | К родителю #63 | Наверх | Cообщить модератору

70. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
Сообщение от Аноним (70), 23-Окт-26, 13:32
LOL. Оно чё, пихало в каждую переменную при вызове библиотечных функций по 64 мега данных? Это уже уровень школоло или уже техдира?
Ответить | Правка | Наверх | Cообщить модератору

	79. "Аnthropic развивает технику для формальной верификации сущес..."	–2 +/–
	Сообщение от Аноним (10), 23-Окт-26, 13:43
	Проспись, какие переменные? Информатику надо было посещать в школе
	Ответить | Правка | Наверх | Cообщить модератору

	83. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (70), 23-Окт-26, 13:45
	Новость дочитать до конца могут не только лишь все?
	Ответить | Правка | Наверх | Cообщить модератору

	84. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (70), 23-Окт-26, 13:47
	Да какая разница, указателями пихать или через другие варианты типа стека. 64 мега всё равно впихуются в функцию в их тестах.
	Ответить | Правка | К родителю #79 | Наверх | Cообщить модератору

	87. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 13:49
	Какие указатели, какой стек? Есть регистры и память - все. Остальное зашито в инструкциях, какие байты куда перекладывать
	Ответить | Правка | Наверх | Cообщить модератору

	115. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (70), 23-Окт-26, 15:37
	Какие именно регистры ты нашёл в статических или динамических сбилженных либах? Оно тестило либы, а не вгруженный в память поток функций же... Либу сначала надо подтянуть, потом впихуть данные... а не в регистры писать указатели.
	Ответить | Правка | Наверх | Cообщить модератору

	226. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Халявщик не корпораст (?), 24-Окт-26, 11:00
	- Оно чё, пихало в каждую переменную... Нет. Оно хромиум пихало везде с поисковиком от гуглирастов и йищё там чивото...
	Ответить | Правка | К родителю #70 | Наверх | Cообщить модератору

72. Скрыто модератором	+2 +/–
Сообщение от Аноним (82), 23-Окт-26, 13:33
> а выявленные расхождения оказались известными граничными случаями. Формальные доказательства без граничных случаев. Они сделали мой день. Насколько нужно быть ..нутыми?
Ответить | Правка | Наверх | Cообщить модератору

90. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
Сообщение от Аноним (90), 23-Окт-26, 13:56
>1.7 миллионов случайно сгенерированных Python-программ интересные у них критерии
Ответить | Правка | Наверх | Cообщить модератору

99. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
Сообщение от опеншлёпивпродакшн (?), 23-Окт-26, 14:24
Получается сначала мы создаём компьютеры и пишем программы, а потом нам нужен ИИ, чтобы во всём этом разобраться. Мне кажется, что игроки железного рынка и игроки ИИ рынка не связаны друг с другом, и сейчас происходит крупное смещение капитала в мире. Возможно даже первые как раз мощно инвестируют во вторых для удержания рычагов власти. В таком случае Сэм Альтман не злодей, а козёл отпущения.
Ответить | Правка | Наверх | Cообщить модератору

	111. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (106), 23-Окт-26, 15:22
	Раньше железо каждый в своем гараже делал, а щас? То же ждет и ПО, готовьтесь, зачем волю давать рабам.
	Ответить | Правка | Наверх | Cообщить модератору

	121. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (10), 23-Окт-26, 16:05
	Ну у нас Нива есть, которую в гараже можно допиливать, а вот другим не повезет
	Ответить | Правка | Наверх | Cообщить модератору

	148. "Аnthropic развивает технику для формальной верификации сущес..."	+3 +/–
	Сообщение от Боевой Петух (?), 23-Окт-26, 18:30
	Наоборот, с появлением AI возникло множество проектов, где один человек пилит проект лучше, чем там, где кожмешки годами топтались на месте.
	Ответить | Правка | К родителю #111 | Наверх | Cообщить модератору

	162. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (162), 23-Окт-26, 20:02
	Никто не мешает пилить Ниву с помощью своей Клавы
	Ответить | Правка | Наверх | Cообщить модератору

	180. "Аnthropic развивает технику для формальной верификации сущес..."	–3 +/–
	Сообщение от Аноним (106), 23-Окт-26, 21:36
	> Наоборот, с появлением AI а зачем с появлением ЫЫ я должен что-то делать? ЫЫ зачем тогда? Вот пусть ЫЫ и делает. То есть, я не должен с помощью ЫЫ пилить проект для распила другого проекта, пусть ЫЫ сразу делает то, что необходимо. А теперь на пальцах, есть куча Г, зачем просить ЫЫ, чтобы напилил палку для разгребания этой кучи, когда он сам (ЫЫ) должен разгребать эту кучу Г.
	Ответить | Правка | К родителю #148 | Наверх | Cообщить модератору

	263. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от анон (?), 25-Окт-26, 17:49
	Множество туду аппов, забрасывающихся как только автору становится скучно.
	Ответить | Правка | К родителю #148 | Наверх | Cообщить модератору

	146. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (146), 23-Окт-26, 18:28
	>а потом нам нужен ИИ, чтобы во всём этом разобраться. Мне кажется, что игроки железного рынка и игроки ИИ рынка не связаны друг с другом Вещь в себе, Когда что то делается не ради чего то, а ради самого делания. Вот только это забавы корпоратов. Дорожает Озу на генерацию котиков, и на всякие хотелки. У людей куча гадждетов, беспроводные наушники, беспроводная мышка, кроссовки с usb, может даже трусы с usb, смартфон с кучей функций аккум которого высаживается за день из за этих Ии и тд фичь. Это все конечно хорошо, вот только люди стали замечать что они больше заряжают все эти гаджеты, чем живут и пользуются.
	Ответить | Правка | К родителю #99 | Наверх | Cообщить модератору

	165. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Смузихеб забывший пароль (?), 23-Окт-26, 20:11
	они более чем связаны и активно вкладываются друг в друга для мощной консолидации капитала
	Ответить | Правка | К родителю #99 | Наверх | Cообщить модератору

107. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
Сообщение от Аноним (107), 23-Окт-26, 15:08
Очень хорошее применение для ИИ.
Ответить | Правка | Наверх | Cообщить модератору

122. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
Сообщение от Xasd1 (?), 23-Окт-26, 16:11
> так как остаются неформализованными > риски, вызванные проблемами с > многопоточностью ну всё, ребята, расходимся.. то есть даже срааное банальное time-of-check-to-time-of-use это не подсвечивает 🙈🙈🙈
Ответить | Правка | Наверх | Cообщить модератору

143. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
Сообщение от Аноним (143), 23-Окт-26, 18:22
Сначала они показали, что параметры какие надо параметры https://www.opennet.ru/opennews/art.shtml?num=66497. Теперь они покажут, что их верификация самая настоящая верификация. Они уверено продвигаются к цели.
Ответить | Правка | Наверх | Cообщить модератору

145. "Аnthropic развивает технику для формальной верификации сущес..."	–2 +/–
Сообщение от Инопланетянин (?), 23-Окт-26, 18:27
Ну вот инженеры-верификаторы тоже напряглись, дверь на улицу приоткрылась и оттуда подул холодный ветерок.
Ответить | Правка | Наверх | Cообщить модератору

	173. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (173), 23-Окт-26, 20:25
	умеешь ты поднять настроение ...
	Ответить | Правка | Наверх | Cообщить модератору

	177. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (146), 23-Окт-26, 21:05
	Понимаю недоумевание разработчиков, с Opennet a, ведь 90%, собирают свой софт, пишут По, а тут такое Ии.
	Ответить | Правка | К родителю #145 | Наверх | Cообщить модератору

	214. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (146), 24-Окт-26, 03:35
	Какая же, Ии модель всетаки, молодец.
	Ответить | Правка | К родителю #145 | Наверх | Cообщить модератору

219. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
Сообщение от Аноним (219), 24-Окт-26, 08:33
> при любых входных данных объёмом до 64 МБ в программе не возникает сбоев. Они решили проблему остановки? Может быть 640 Кб хватит всем?
Ответить | Правка | Наверх | Cообщить модератору

	228. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (146), 24-Окт-26, 12:49
	Купить Mac Studio на чипе Apple Silicon с 128 ГБ или 192 ГБ объединенной памяти, либо собрать ПК с 256 Гб серверной Ddr5 ОЗУ. Это позволяет запускать тяжелые Ии-модели, хоть и медленнее, чем на видеокартах, и быть крутым. https://habr.com/ru/companies/selectel/articles/1030298 Но ведь меньше 32 Гб Озу - это для печатных машинок. Чтобы запускать Antropic, у которой, >при любых входных данных объёмом до 64 МБ в программе не возникает сбоев
	Ответить | Правка | Наверх | Cообщить модератору

	231. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
	Сообщение от Инопланетянин (?), 24-Окт-26, 13:30
	> либо собрать ПК с 256 Гб серверной Ddr5 ОЗУ. А цену можно сразу озвучить? Хотя бы просто на память отдельно?
	Ответить | Правка | Наверх | Cообщить модератору

	232. Скрыто модератором	–1 +/–
	Сообщение от Аноним (146), 24-Окт-26, 13:36
	https://www.ixbt.com/news/2026/04/19/kompanija-obnovila-serv... Да, ведь Озу сейчас всем раздают так. А ты что не знал, ты что покупаешь чтоли. Люди даже поделки из Ddr серверной делают, не знаю куда девать. Ее ведь щас как гуталина у кота, ну просто прям много.
	Ответить | Правка | Наверх | Cообщить модератору

	234. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (41), 24-Окт-26, 14:30
	Ну вот в соседих темах php сломали видать как раз на 65-ом метре.
	Ответить | Правка | К родителю #219 | Наверх | Cообщить модератору

	236. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (146), 24-Окт-26, 15:53
	Если Ии Anthropic ломается на 65 МБ, значит, они просто не умеют пользоваться архиватором Arj с разбивкой на тома. Неси дискету 3.5, перекинем туда винду, и еще и место под Php останется.
	Ответить | Правка | Наверх | Cообщить модератору

262. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
Сообщение от Аноним (262), 25-Окт-26, 15:19
Ну вот формально верифицируют существующее ПО, и Раст оказывается вообще не нужен как лишняя сущность. К тому же в эпоху генерации кода ИИ куда важнее читабельность кода, а с этим у Раста проблемы.
Ответить | Правка | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема