Cool post. I don’t fully understand what a code contract is but appreciate the advice. I have settled on a similarly light weight /agile folder when I keep my roadmap.md with epics and sprints.
It's a set of asserts that are a part of the type signature. Requires are asserts on the inputs, ensures are asserts on the outputs.
Depending on your backend you either ignore them, check them all of the time, some of the time, or have SMT-solvers prove that if you uphold the first one all else must follow.
If you're interested in the last one, have a look at Dafny[0]
It's a set of asserts that are a part of the type signature. Requires are asserts on the inputs, ensures are asserts on the outputs.
Depending on your backend you either ignore them, check them all of the time, some of the time, or have SMT-solvers prove that if you uphold the first one all else must follow.
If you're interested in the last one, have a look at Dafny[0]
[0] https://dafny.org/