<story><title>ZZ is a modern formally provable dialect of C</title><url>https://github.com/aep/zz</url></story><parent_chain></parent_chain><comment><author>MaxBarraclough</author><text>I find the basic idea of this project to be very compelling - I was thinking aloud on HN recently and arrived at roughly the idea this project is implementing. [0]&lt;p&gt;With that said, I really dislike the way they&amp;#x27;re describing their project.&lt;p&gt;When I read &lt;i&gt;safe dialect of C&lt;/i&gt;, I first assumed they meant they had developed a safe subset of C, or perhaps a very similar language, like OpenCL C [1]. Instead, they developed a new language which isn&amp;#x27;t C at all. Nothing wrong with that, but if I don&amp;#x27;t instantly recognise the syntax as C, I wouldn&amp;#x27;t call it a C dialect.&lt;p&gt;They also put &lt;i&gt;formally provable dialect of C&lt;/i&gt;. Their language compiles to C code which is guaranteed to be free from undefined behaviour. This is not the same thing as a language where hard guarantees can be made about program behaviour, such as SPARK [2] or Dafny [3].&lt;p&gt;If the authors are reading this, I urge you to improve your project summary. Your language does not allow me to prove program correctness, instead it protects me from C&amp;#x27;s undefined behaviour. That&amp;#x27;s still a great idea! Please make this clear!&lt;p&gt;[0] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;news.ycombinator.com&amp;#x2F;item?id=22102658&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;news.ycombinator.com&amp;#x2F;item?id=22102658&lt;/a&gt;&lt;p&gt;[1] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;OpenCL#OpenCL_C_language&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;OpenCL#OpenCL_C_language&lt;/a&gt;&lt;p&gt;[2] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;SPARK_(programming_language)&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;SPARK_(programming_language)&lt;/a&gt;&lt;p&gt;[3] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;Dafny&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;Dafny&lt;/a&gt;</text></comment>
<story><title>ZZ is a modern formally provable dialect of C</title><url>https://github.com/aep/zz</url></story><parent_chain></parent_chain><comment><author>pjc50</author><text>This is a great achievement in making formal methods accessible in pragmatic terms - something that actually works and can be used by normal humans.&lt;p&gt;Would be nice to have an actual microcontroller example.&lt;p&gt;&amp;gt; The standard library is fully stack based and heap allocation is strongly discouraged&lt;p&gt;:&amp;#x2F; - I can see why this is done, as it&amp;#x27;s hard, so banning it to make the problem tractable works. But it&amp;#x27;s also quite inconvenient. On the other hand, &amp;quot;MISRA C:2004, 20.4 - Dynamic heap memory allocation shall not be used.&amp;quot;</text></comment>