[derkha]

By calling the verification 'simple' myself, I concede that it may also be _simplistic_ in parts. Perhaps I should have emphasized that this project is mostly about algorithmic correctness currently. A bug in the compiler backend would not be a bug in the algorithm, and neither would I call a function unexpectedly panicking on more than 2^63 elements an algorithmic bug. And if you compile your Rust program with overflow checks (default in debug mode), the verification can still guarantee partial correctness: If it does not panic due to some overflow, the result is correct.

You're correct in that what I'm constructing is some form of Dynamic Single Assignment. But together with the eradication of mutable references (and perhaps other effects in the future), it felt better to me to describe the transformation from the purity aspect.