Technique: Proof types to ensure preconditions
Consider a library using hidden global state that needs to be initialized by calling an initialization function. If you don’t call the function before you start using the library, it crashes.
How do you design the library in such a way that it is impossible to use it before initialization?
One idea is to use a technique where you create a special proof type, which needs to be passed as an additional parameter. Let’s look at it in more detail.» read more »