<story><title>Nagini: A Static Verifier for Python [pdf]</title><url>http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&amp;id=EilersMueller18.pdf</url></story><parent_chain></parent_chain><comment><author>btown</author><text>This is really, really cool. It&amp;#x27;s on github at &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;marcoeilers&amp;#x2F;nagini&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;marcoeilers&amp;#x2F;nagini&lt;/a&gt; and you can see examples of the syntax here: &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;viper.ethz.ch&amp;#x2F;nagini-examples&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;viper.ethz.ch&amp;#x2F;nagini-examples&amp;#x2F;&lt;/a&gt;&lt;p&gt;In the same way that Python&amp;#x27;s (and Flow&amp;#x2F;Typescript&amp;#x27;s) typing lets you describe argument and return types with no more effort&amp;#x2F;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&amp;#x27;s a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It&amp;#x27;s the type of thing that there&amp;#x27;s no reason &lt;i&gt;not&lt;/i&gt; to use.&lt;p&gt;It&amp;#x27;s powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;people.inf.ethz.ch&amp;#x2F;summersa&amp;#x2F;wiki&amp;#x2F;lib&amp;#x2F;exe&amp;#x2F;fetch.php?media=papers:viper-vmcai16.pdf&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;people.inf.ethz.ch&amp;#x2F;summersa&amp;#x2F;wiki&amp;#x2F;lib&amp;#x2F;exe&amp;#x2F;fetch.php?me...&lt;/a&gt; . Very smart stuff around tracking read&amp;#x2F;write dependencies on variables in a programmer-friendly way.</text></comment>
<story><title>Nagini: A Static Verifier for Python [pdf]</title><url>http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&amp;id=EilersMueller18.pdf</url></story><parent_chain></parent_chain><comment><author>Animats</author><text>Classic, and nicely done.&lt;p&gt;They did something right that&amp;#x27;s rarely done - their verification extensions to Python are Pythonic. They don&amp;#x27;t use a separate language for invariants and assertions, and they don&amp;#x27;t put the assertions in comments. The assertions are thus part of the program.</text></comment>