++

Проблема только то что мы не знаем есть ли там ощибка

И судя по размеру кода вряд ли когда нибудь узнаем (окончательно)

Мы знаем что там когда-то не было ошибок. Формально доказывали.

“Soundness is a statement about whether all possible uses of a library or language feature uphold the intended invariants. In other words it describes functionality that cannot be misused, neither by mistake nor maliciously.
It is worth internalizing this understanding of soundness when evaluating soundness bugs; they are a very different sort of bug than typical exploitable memory safety vulnerabilities like use-after-free or buffer overflows. When a library is unsound, it tells you the library is possible to misuse in a way that could be a vulnerability, but it does not tell you that any code has already misused the library in such a way.
In my experience discovering unsound library code in my work codebase, so far it's always only been hypothetical contrived code that could be broken; the existing uses of the unsound libraries have always been correct. We fix the soundness bugs to ensure it remains that way as the codebase scales.”

https://docs.rs/dtolnay/0.0.7/dtolnay/macro._03__soundness_bugs.html

Я пытаюсь понять как можно описать инвариант в случае с Len. Сказать что он unsafe означает что он нарушает принятые в rust safety rules, но это же строго говоря не так

Не нарушает а может привести к нарушению

Потому и ансейф

Но вообще мне все это кажется натягивание совы

Есть предел выразительности системы сейф/ансейф

На произвольный контракт ее не распространить

И помечать все что невыразимо ансейфом тоже не стоит

+++

+++

Дело в том что unsafe{} находится в других местах и использует len. А т.к. unsafe относится только к функциям... то это запутывает

На распарсил слова мейк ду

Но выглядит прикольно ))

Модуль node из BTreeMap.

Было бы конечно здорово если бы прикрутили formal verification, но такого насколько я помню не делали ни для одного серьезного языка программирования