Earlier quoted context omitted.
Coding with contracts has always been interesting to me but I haven't had the option/time to try it seriously in a project. I assume you've had experience with it, how much productivity/code maintanability you gain compared to not using it (or using type annotations)?
In my anecdotal experience, it takes very little time for juniors to pick up adding contracts to their code. You need to grasp implication, equivalence, exclusive or, and get used to declarative code, but then it's easy. (I often compare it to SQL.) I find contracts personally super useful as I can express a lot of relationships in the code trivially and have them automatically verified. For example, when this input…
I tend to limit myself to simple contracts and do table tests for the complex cases to reap the benefits of the both approaches.