In the same way that Python's (and Flow/Typescript's) typing lets you describe argument and return types with no more effort/characters than typing a comment, this lets you describe invariants and assertions exactly where you normally would with comments, including invariants on each element of a sequence... and instantly get static typing. I believe there's a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It's the type of thing that there's no reason not to use.
It's powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?me... . Very smart stuff around tracking read/write dependencies on variables in a programmer-friendly way.
Assertions, combined with highly granular code coverage (which most [all?] Python coverage libraries can only do at a line level, so this isn't really sufficient), can almost get you to a point where you're confident that all your asserted invariants are true for all inputs.
Statically checking/proving that those invariants will hold, regardless of inputs, is a huge step up in that level of confidence.
In the same way that Python's (and Flow/Typescript's) typing lets you describe argument and return types with no more effort/characters than typing a comment, this lets you describe invariants and assertions exactly where you normally would with comments, including invariants on each element of a sequence... and instantly get static typing. I believe there's a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It's the type of thing that there's no reason not to use.
It's powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?me... . Very smart stuff around tracking read/write dependencies on variables in a programmer-friendly way.