В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Lietuvos Traktorius 🚜 ~ @tractorlt

158 membersпожаловаться на группу
2020 July 19

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
чтобы использовать прямо в процессе разработки, в идеале логику надо встроить в систему типов, но для императивных программ это открытая задача
источник
22:11пожаловаться#1

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
скорее всего конечно это какая то разновидность субструктурной логики аля раст
источник
22:12пожаловаться#2

GN

Grey Nomad in Lietuvos Traktorius 🚜 ~ @tractorlt
Эм.
А если попроще?
источник
22:16пожаловаться#3

S

Sergejus in Lietuvos Traktorius 🚜 ~ @tractorlt
источник
22:22пожаловаться#4

VJ

Valdis Jansons in Lietuvos Traktorius 🚜 ~ @tractorlt
AnimatedSticker.tgs
(7.09 Кб)
источник
22:22пожаловаться#5

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
Grey Nomad
Эм.
А если попроще?
автоматический прувер запускают в CI, систему типов при разработке, ручной прувинг это отдельный кропотливый процесс (примерно в 10 раз медленнее обычного программирования по усреднённым оценкам)
источник
22:26пожаловаться#6

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
есть ещё верификация моделей, ей занимаются как правило до разработки, чтобы заранее увидеть слабые места в дизайне
источник
22:27пожаловаться#7

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
всё это - разные вычислительные реализации каких либо логических систем
источник
22:28пожаловаться#8

GN

Grey Nomad in Lietuvos Traktorius 🚜 ~ @tractorlt
И какого рода разработки юзают такие пруверы? Явно не масс-продакшн.
источник
23:34пожаловаться#9

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
Grey Nomad
И какого рода разработки юзают такие пруверы? Явно не масс-продакшн.
а вы гляньте https://fbinfer.com/
Fbinfer
Infer Static Analyzer | Infer | Infer
A tool to detect bugs in Java and C/C++/Objective-C code before it ships
источник
23:34пожаловаться#10

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
там снизу есть список пользователей
источник
23:35пожаловаться#11

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
или вопрос был про ручной прувинг?
источник
23:38пожаловаться#12

GN

Grey Nomad in Lietuvos Traktorius 🚜 ~ @tractorlt
Ну в том списке не последние парни на деревне. Но маркетологи Инфера последних бы и не выбрали.

А причем тут логические системы? MaybeNull анализаторы даже PVS-ники реализуют (не к ночи будут помянуты).
источник
23:39пожаловаться#13

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
Grey Nomad
Ну в том списке не последние парни на деревне. Но маркетологи Инфера последних бы и не выбрали.

А причем тут логические системы? MaybeNull анализаторы даже PVS-ники реализуют (не к ночи будут помянуты).
инфер это отдел внутри фейсбука (точнее стартап, купленный им в 2013)
источник
23:40пожаловаться#14

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
поэтому тулза и называется FB Infer
источник
23:40пожаловаться#15

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
логические системы потому что для более-менее полноценного анализа нужна какая то логическая модель кода
источник
23:43пожаловаться#16

GN

Grey Nomad in Lietuvos Traktorius 🚜 ~ @tractorlt
Abstract Syntax Tree не пойдет?
источник
23:43пожаловаться#17

GN

Grey Nomad in Lietuvos Traktorius 🚜 ~ @tractorlt
Ну, или Semantic Model, раз уж мы про CI-time инструмент.
источник
23:44пожаловаться#18

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
ast это условно говоря только система термов, а еще нужны её свойства, правила преобразования
источник
23:46пожаловаться#19

AG

Alex Gryzlov in Lietuvos Traktorius 🚜 ~ @tractorlt
в каком смысле semantic model?
источник
23:46пожаловаться#20