Comment by fooker

This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?