История изменений
Исправление quantum-troll, (текущая версия) :
Логика разделения позволяет строго рассуждать о таких вещах: https://www.cs.cmu.edu/~jcr/seplogic.pdf
Кстати, для раста есть вот такая штука: https://github.com/xldenis/creusot. И она даже юзабельна, CreuSAT ей верифицировали.
Исходная версия quantum-troll, :
Логика разделения позволяет строго рассуждать о таких вещах: https://www.cs.cmu.edu/~jcr/seplogic.pdf
Кстати, для раста есть вот такая штука: https://github.com/xldenis/creusot. И она даже юзабельна, CreuSAT её верифицировали.