<story><title>Coq-based synthesis of Scala programs which are correct-by-construction [pdf]</title><url>https://cedric.cnam.fr/fichiers/art_4027.pdf</url></story><parent_chain></parent_chain><comment><author>tehmillhouse</author><text>If you&amp;#x27;re interested in this kind of thing, note that Coq can also extract code in Haskell, Scheme and OCaml.&lt;p&gt;If Coq&amp;#x27;s not quite your cup of tea, Isabelle&amp;#x2F;HOL is another proof assistant with amazing (dare I say superior?) tooling and automation, and it supports code extraction in SML, OCaml, Haskell and Scala.&lt;p&gt;Microsoft Research&amp;#x27;s Lean theorem prover is also promising in this regard. Work is almost complete on native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code. (see &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover&amp;#x2F;lean&amp;#x2F;pull&amp;#x2F;1241&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover&amp;#x2F;lean&amp;#x2F;pull&amp;#x2F;1241&lt;/a&gt; for progress)&lt;p&gt;(Note that none of those code extractors are verified to be correct themselves, lacking a formalization of the target language&amp;#x27;s semantics. You don&amp;#x27;t get a mathematical proof that the code you&amp;#x27;re running does what you specified, but you get &lt;i&gt;pretty damn close&lt;/i&gt;.)</text></comment>
<story><title>Coq-based synthesis of Scala programs which are correct-by-construction [pdf]</title><url>https://cedric.cnam.fr/fichiers/art_4027.pdf</url></story><parent_chain></parent_chain><comment><author>pharrington</author><text>The source repo is at &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;JBakouny&amp;#x2F;Scallina&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;JBakouny&amp;#x2F;Scallina&lt;/a&gt;</text></comment>