andrewthad / linear-containers

Containers supporting in-place modification
BSD 3-Clause "New" or "Revised" License
5 stars 1 forks source link

Verification of Correctness #1

Open andrewthad opened 5 years ago

andrewthad commented 5 years ago

The Static vs Dynamic trick that this library seems sound based on my informal reasoning. It would be nice to verify that it is actually sound. I am not capable of a rigorous proof, but maybe someone else could.

andrewthad commented 5 years ago

With https://github.com/andrewthad/linear-containers/pull/6, I've added a rough explanation of how static and dynamic references work. This should hopefully help anyone who is trying to understand what's going on.