Большое спасибо за описание механизма прав в Zircon! Доказал их корректность и поигрался с ними в Isabelle/HOL, далее можно будет уже лепить реальный код для эмулятора .
Ну так WhyML далеко не всесилен и может разве что тактики подобрать, полное доказательство - это уже вручную. А Z3/CVC - хорошо, много лучше, чем ничего, но не идеал. Но идея, конечно, хорошая. Правда, если кому-то реально нужно, возьмет Lean4 с завтипами и HoTT(вроде бы) + будет иметь уже готовый к пуску бинарь. А Frama очень многого не поймет в простом сишном коде, афаир, уж проще сразу Isabelle/C или Autocorres :)
Перед реализацией такие вещи моделируются, ваш коллега из Яндекса некоторое время назад как раз и рассказывал здесь об опыте применения TLA+ для решения проблем инфраструктуры
Лучший линукс - это фря, лучшая фря - это циска (с) поговорка начала нулевых
Большое спасибо за описание механизма прав в Zircon! Доказал их корректность и поигрался с ними в Isabelle/HOL, далее можно будет уже лепить реальный код для эмулятора .
Деды могли!
Большой молодец!
Нет формального обоснования - алгоритм в помойку
Очень интересно, пишите ещё!
Нет, не гуглю, вполне себе юзаю. Речь о другом, но объяснять не буду - многовато чести
Ну так WhyML далеко не всесилен и может разве что тактики подобрать, полное доказательство - это уже вручную. А Z3/CVC - хорошо, много лучше, чем ничего, но не идеал. Но идея, конечно, хорошая. Правда, если кому-то реально нужно, возьмет Lean4 с завтипами и HoTT(вроде бы) + будет иметь уже готовый к пуску бинарь. А Frama очень многого не поймет в простом сишном коде, афаир, уж проще сразу Isabelle/C или Autocorres :)
Итерация свойственна человеку, рекурсия божественна.
Перед реализацией такие вещи моделируются, ваш коллега из Яндекса некоторое время назад как раз и рассказывал здесь об опыте применения TLA+ для решения проблем инфраструктуры
Отлично! С надоями-то нормально всё?
Можно попробовать заюзать чего с зависимыми и уточненными типами - вдруг полегчает. F* там или Агду
На святое замахнулись! Вообще, правильно, такие системы должны очень жестко проверяться. Шлите привет Вирдингу, Декеру и Вильямсу :)
Если с песнями - то опенок еще торт!
Автор задается очень правильной философско-инженерной мыслью, из которой вытекают очень интересные и важные выводы :)
Диалог в библиотеке:
- Мне, пожалуйста, "Эффективная работа в Microsoft Windows"
-Фантастика - на втором этаже!
Кроме тестов ,есть еще и моделирование, и верификация... :)
Никаких иных методик, кроме тестов, не применяется?
Ну хоть не в стиле Луговского спорит - и то ладно :)
Книжка хорошая, тетенька молодец