Nice post! I'm relatively new to Nim, hadn't found out about the side effects tracking yet.
Also you state that 'the contract shields our code from the bug' but don't mention what happens at compile-time or runtime in the example (i.e. what is the error message you will get).
Vanilla assert error, as the DbC uses in general.
Maybe on the future it can self-document the contract using CommentStmt.
We're a place where coders share, stay up-to-date and grow their careers.
We strive for transparency and don't collect excess data.