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