|
Sounds scary?
The title frightened me, but the contents is even more fearful ;-)
John Reynolds demonstrates "an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.".
Looks like another formal approach to impurity. And I thought that monads are evil...
Though this paper seems to target compiler implementers, I find it useful for language designers as well.
| 
A Logic for Shared Mutable Data Structures