<story><title>Show HN: Dependently typed language for proofs that you can implement in one day</title><url>https://github.com/caotic123/PomPom-Language</url></story><parent_chain><item><author>dwohnitmok</author><text>I find the often ML-inspired syntax too high of a bar for most programmers to clear when being introduced to a language.&lt;p&gt;I think a syntax more similar to something like what is introduced here: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;shuangrimu.com&amp;#x2F;posts&amp;#x2F;language-agnostic-intro-to-dependent-types.html&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;shuangrimu.com&amp;#x2F;posts&amp;#x2F;language-agnostic-intro-to-depe...&lt;/a&gt; more accessible for a lot of programmers.&lt;p&gt;I separately think that proofs are actually a bit overblown when it comes to dependent types and that dependent types are most useful for specification, but often times could benefit from &amp;quot;fake&amp;quot; implementations.</text></item></parent_chain><comment><author>Zababa</author><text>I agree that ML-style function signature is probably the best and most readable. `name: type` is a lot better than `type name`. I would argue that `match x with` would be better than `case x of`, to highlight that pattern matching is different than your usual switch. Calling out explicitely the contructors with `contructors` is a good idea, I think it can make things easier for new people.&lt;p&gt;Edit: I wonder if it would help to also have a record type. Enum allows you to have full ADTs, but named tuples are often more useful than regular tuples.</text></comment>
<story><title>Show HN: Dependently typed language for proofs that you can implement in one day</title><url>https://github.com/caotic123/PomPom-Language</url></story><parent_chain><item><author>dwohnitmok</author><text>I find the often ML-inspired syntax too high of a bar for most programmers to clear when being introduced to a language.&lt;p&gt;I think a syntax more similar to something like what is introduced here: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;shuangrimu.com&amp;#x2F;posts&amp;#x2F;language-agnostic-intro-to-dependent-types.html&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;shuangrimu.com&amp;#x2F;posts&amp;#x2F;language-agnostic-intro-to-depe...&lt;/a&gt; more accessible for a lot of programmers.&lt;p&gt;I separately think that proofs are actually a bit overblown when it comes to dependent types and that dependent types are most useful for specification, but often times could benefit from &amp;quot;fake&amp;quot; implementations.</text></item></parent_chain><comment><author>caotic123</author><text>The syntax you presented is &lt;i&gt;really&lt;/i&gt; very accessible. Of course, it makes things a little more verbose, but I think you are right, the path for bringing more attention to dependent types is probably making more accessible also. Btw, great article I will have a more detailed look after.</text></comment>