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

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

Сообщения

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

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

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

	21. Скрыто модератором	+1 +/–
	Сообщение от miu (?), 23-Окт-26, 11:24
	А также тире и дефис.
	Ответить | Правка | Наверх | Cообщить модератору

	22. Скрыто модератором	+/–
	Сообщение от Bottle (?), 23-Окт-26, 11:29
	Дальше последует применение кавычек-«ёлочек» и „лапок“, как и применение точек в конце комментариев.
	Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

	73. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Аноним (73), 23-Окт-26, 13:33
	А ещё ЕИ таки выучит правило правописания приставок, оканчивающихся на "с" и "з" https://ruhomeschool.ru/russkiiyazyk/z-i-s-na-koncze-pristavok
	Ответить | Правка | К родителю #24 | Наверх | Cообщить модератору

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

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

	133. Скрыто модератором	+/–
	Сообщение от Пыщь (?), 23-Окт-26, 17:34
	а он ещё тот п.. пустобрёх. Тяжко выдавать из себя образованного, когда выхлоп невросетей из всех щелей сквозит.
	Ответить | Правка | Наверх | Cообщить модератору

	138. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от pic (??), 23-Окт-26, 18:07
	И какой же у неё смысл?
	Ответить | Правка | К родителю #128 | Наверх | Cообщить модератору

	26. "Аnthropic развивает технику для формальной верификации сущес..."	–3 +/–
	Сообщение от pic (??), 23-Окт-26, 11:46
	В русском языке традиционно применяются французские «ёлочки», а для кавычек внутри кавычек и при письме от руки — немецкие „лапки“ или "скандинавские". В рукописном тексте не применяются кавычки "ёлочки", используются "лапки". И обозначают они одно и тоже - цитату, прямую речь, отсылку.
	Ответить | Правка | К родителю #6 | Наверх | Cообщить модератору

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

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

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

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

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

	140. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от pic (??), 23-Окт-26, 18:13
	https://ru.wikipedia.org/wiki/Кавычки Читай умник.
	Ответить | Правка | К родителю #102 | Наверх | Cообщить модератору

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

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

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

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

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

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

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

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

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

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

	103. Скрыто модератором	+/–
	Сообщение от Пыщь (?), 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ообщить модератору

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

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

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

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

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

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

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

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

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

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

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

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

	167. "Аnthropic развивает технику для формальной верификации сущес..."	+/–
	Сообщение от черпало (?), 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ообщить модератору

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

	80. "Аnthropic развивает технику для формальной верификации сущес..."	+1 +/–
	Сообщение от Аноним (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 развивает технику для формальной верификации сущес..."	+/–
	Сообщение от Инопланетянин (?), 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ообщить модератору

16. Скрыто модератором	+/–
Сообщение от Метрика (?), 23-Окт-26, 11:10
Снова раст, снова нейрослоп
Ответить | Правка | Наверх | Cообщить модератору

	20. Скрыто модератором	+/–
	Сообщение от Аноним (20), 23-Окт-26, 11:23
	> Снова раст, снова нейрослоп Да, вы абсолютно правы (с) Пока Настоящие СИшники нагадили в ПХП так, что половина интернета продырявилась, нехорошие растеры пытаются сделать формальную верификацию. Как им не стыдно!! Лучше бы наовнячили пару выходов за пределы буфера как уважаемые диды. assisted by Claude
	Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

38. "Аnthropic развивает технику для формальной верификации сущес..."	+2 +/–
Сообщение от Аноним (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ообщить модератору

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ообщить модератору

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ообщить модератору

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

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

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

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

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

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

	162. "Аnthropic развивает технику для формальной верификации сущес..."	–1 +/–
	Сообщение от Аноним (162), 23-Окт-26, 20:02
	Никто не мешает пилить Ниву с помощью своей Клавы
	Ответить | Правка | Наверх | 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.dev/opennews/art.shtml?num=66497. Теперь они покажут, что их верификация самая настоящая верификация. Они уверено продвигаются к цели.
Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

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