<story><title>Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains</title><url>https://arend-lang.github.io/</url></story><parent_chain></parent_chain><comment><author>jey</author><text>Wow, JetBrains has a whole HoTT and Dependent Types Research Group: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;research.jetbrains.org&amp;#x2F;groups&amp;#x2F;group-for-dependent-types-and-hott&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;research.jetbrains.org&amp;#x2F;groups&amp;#x2F;group-for-dependent-ty...&lt;/a&gt;</text></comment>
<story><title>Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains</title><url>https://arend-lang.github.io/</url></story><parent_chain></parent_chain><comment><author>namelosw</author><text>Wow. Finally a prover with serious IDE support.&lt;p&gt;I always believe this field would be very useful and evolving steadily in the industry. It just doesn&amp;#x27;t attract eyeballs like machine learning and blockchains.</text></comment>