Modules and coeffects
Next version of Lever requires that module contents are verified invariant. I emphasis verified because the code that enforces the rule will be incomplete; it is not able to correctly identify every invariant object.
The constraint makes it easier to do proofs and verify behaviors from the code. You do not need to worry whether two unrelated programs would crosstalk through modules they use by inadvertendly changing their contents. Static analysers and other tools will have more invariants to work with.
There are few reasons why I kept away from doing it this way in the first place. The main reason was the concern of not being able to do live programming. Another reason was that all module contents are not invariant.
I was thinking by doing live programming through changing program contents while it was running. I realised it would be much more reliable to define clearly described boundaries where software can save the state and restore itself with a new version of the program.
The variant parts of the modules can be enclosed into coeffects. This also makes those variant parts more useful. There are several immediate uses for this such as tracking source location during parsing, logging, selecting shared libraries in use.