С той поры Cockroach применяют TLA+ и стали сильно стабильнее. Собственно, недавно отловил много багов собственноручно в MongoDB и ее third party-зависимостях
Очень хорошо, автор молодец. Как вижу, используете TLA-плагин для VSCode вместо штатной IDE - не подскажете, сталкивались ли с ограничениями плагина?
Будет ли статья про Isabelle/HOL ?:) Хорошо было бы осветить в статье проблему комбинаторного взрыва и решение данного вопроса с помощью proof assistant-ов, но это уже сильно раздувающая статью тема, конечно.
Большое спасибо за описание механизма прав в Zircon! Доказал их корректность и поигрался с ними в Isabelle/HOL, далее можно будет уже лепить реальный код для эмулятора .
Ну так WhyML далеко не всесилен и может разве что тактики подобрать, полное доказательство - это уже вручную. А Z3/CVC - хорошо, много лучше, чем ничего, но не идеал. Но идея, конечно, хорошая. Правда, если кому-то реально нужно, возьмет Lean4 с завтипами и HoTT(вроде бы) + будет иметь уже готовый к пуску бинарь. А Frama очень многого не поймет в простом сишном коде, афаир, уж проще сразу Isabelle/C или Autocorres :)
Перед реализацией такие вещи моделируются, ваш коллега из Яндекса некоторое время назад как раз и рассказывал здесь об опыте применения TLA+ для решения проблем инфраструктуры
Спасибо, Витя, пиши еще!
Ну что ж, пожелаем успехов
С той поры Cockroach применяют TLA+ и стали сильно стабильнее. Собственно, недавно отловил много багов собственноручно в MongoDB и ее third party-зависимостях
Пьер - молодец, переводчик - тоже!
Спасибо! А если бумажная версия куплена, можно ли заиметь PDF? Неудобно большую руками читать, как ни крути. Ногами - тоже не очень
Что такое "операционная система Linux"?
Пожалуйста, пишите ещё, как наказывал Луговский
Автор, пишите еще!
Очень хорошо, автор молодец. Как вижу, используете TLA-плагин для VSCode вместо штатной IDE - не подскажете, сталкивались ли с ограничениями плагина?
Будет ли статья про Isabelle/HOL ?:) Хорошо было бы осветить в статье проблему комбинаторного взрыва и решение данного вопроса с помощью proof assistant-ов, но это уже сильно раздувающая статью тема, конечно.
Лучший линукс - это фря, лучшая фря - это циска (с) поговорка начала нулевых
Большое спасибо за описание механизма прав в Zircon! Доказал их корректность и поигрался с ними в Isabelle/HOL, далее можно будет уже лепить реальный код для эмулятора .
Деды могли!
Большой молодец!
Нет формального обоснования - алгоритм в помойку
Очень интересно, пишите ещё!
Нет, не гуглю, вполне себе юзаю. Речь о другом, но объяснять не буду - многовато чести
Ну так WhyML далеко не всесилен и может разве что тактики подобрать, полное доказательство - это уже вручную. А Z3/CVC - хорошо, много лучше, чем ничего, но не идеал. Но идея, конечно, хорошая. Правда, если кому-то реально нужно, возьмет Lean4 с завтипами и HoTT(вроде бы) + будет иметь уже готовый к пуску бинарь. А Frama очень многого не поймет в простом сишном коде, афаир, уж проще сразу Isabelle/C или Autocorres :)
Итерация свойственна человеку, рекурсия божественна.
Перед реализацией такие вещи моделируются, ваш коллега из Яндекса некоторое время назад как раз и рассказывал здесь об опыте применения TLA+ для решения проблем инфраструктуры
Отлично! С надоями-то нормально всё?