Comment by bluGill

I'm looking forward to seeing where these go in the future. Can solvers prove my code correct (at least in some trivial cases)? What should happen in a unit test (sometimes I want to test that my program handles out of range values, sometimes it is expensive top check and so I put the contract in to avoid the check at runtime...) Can/should the optimizer account for contracts (same question as unit tests).