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