<story><title>Verified Programming in F*: A Tutorial</title><url>http://fstar-lang.org/tutorial/</url></story><parent_chain></parent_chain><comment><author>adsharma</author><text>Also see: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;rise4fun.com&amp;#x2F;fstar&amp;#x2F;tutorial&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;rise4fun.com&amp;#x2F;fstar&amp;#x2F;tutorial&lt;/a&gt;&lt;p&gt;Even though this sounds like formal verification gobbledygook, there is some information of practical value there.&lt;p&gt;How many JSON validators have you seen in python and javascript? Why can&amp;#x27;t the static type checkers like mypy and pyright do this for us?&lt;p&gt;The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you&amp;#x27;re assigning a string to an int, but not if you&amp;#x27;re assigning 200 to an int whose type allows only numbers in [10, 100].&lt;p&gt;So one creates a new class with a validate() method, which is completely unnecessary and doesn&amp;#x27;t protect you against integer overflows elsewhere in the code.&lt;p&gt;F* and OCaml derivatives are our best hope in developing a type system which perform these types of common checks in one integrated framework via refinement types and dependent types.&lt;p&gt;Hopefully, one day that work can hit mainstream languages like python, javascript and whatever ends up being the system programming language of choice replacing C in the coming years.</text></comment>
<story><title>Verified Programming in F*: A Tutorial</title><url>http://fstar-lang.org/tutorial/</url></story><parent_chain></parent_chain><comment><author>keyle</author><text>I&amp;#x27;m confused. Is this either very new or very old? What&amp;#x27;s the context?</text></comment>