<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On 17 February 2018 at 23:36, Karthikeyan Bhargavan <span dir="ltr"><<a href="mailto:karthik.bhargavan@gmail.com" target="_blank">karthik.bhargavan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">Looks nice.<div><br></div><div>I’ve been wondering about how to balance between higher-order functions, generator/list comprehension syntax, and standard imperative loops.</div><div>It seems to me that the first is more natural for most verification languages, whereas the last may be most natural to programmers/spec authors.</div><div>Are comprehensions a good middle-ground? Are they even more confusing to programmers?</div></div></blockquote><div><br></div><div>Comprehensions are pretty widely used these days, IMO, and are easily understood as a shorthand for a particular kind of loop. So, I would not imagine they're going to confuse most programmers.</div><div><br></div><div>Of course, they are less flexible than loops. :-)</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><div><br></div><div>-Karthik</div><div><div><br><blockquote type="cite"><span class=""><div>On 17 Feb 2018, at 23:04, Adam Chlipala <<a href="mailto:adamc@csail.mit.edu" target="_blank">adamc@csail.mit.edu</a>> wrote:</div><br class="m_-5806363339123054361Apple-interchange-newline"></span><div><span class="">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF">
    One small suggestion for Poly1305: I've created <a href="https://github.com/HACS-workshop/hacspec/pull/6" target="_blank">a PR</a>
    that redoes polynomial evaluation with comprehensions, in a
    different way.  I expect this version should be easier to translate
    to backends we care about.<br>
    <br>
    What do you think?<br>
  </div></span><span class="">

______________________________<wbr>_________________<br>Hacspec mailing list<br><a href="mailto:Hacspec@moderncrypto.org" target="_blank">Hacspec@moderncrypto.org</a><br><a href="https://moderncrypto.org/mailman/listinfo/hacspec" target="_blank">https://moderncrypto.org/<wbr>mailman/listinfo/hacspec</a><br></span></div></blockquote></div><br></div></div><br>______________________________<wbr>_________________<br>
Hacspec mailing list<br>
<a href="mailto:Hacspec@moderncrypto.org">Hacspec@moderncrypto.org</a><br>
<a href="https://moderncrypto.org/mailman/listinfo/hacspec" rel="noreferrer" target="_blank">https://moderncrypto.org/<wbr>mailman/listinfo/hacspec</a><br>
<br></blockquote></div><br></div></div>