<div dir="ltr"><div>I agree, comprehensions 

should be well known and not an issue for programmers/spec writers. But I'm not sure if they are flexible enough. We can of course allow both, loops and comprehensions, but that'll make the language more complex.<br><br></div>Adam, do you want to update your PR to leave the other versions in so we can compare all three of them?<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 18, 2018 at 8:25 AM, Ben Laurie <span dir="ltr"><<a href="mailto:benl@google.com" target="_blank">benl@google.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote"><span class="">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></span><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><span class=""><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><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_-1647560380770696228m_-5806363339123054361Apple-interchange-newline"></span><div><span>
  
    
  
  <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>

______________________________<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/mailm<wbr>an/listinfo/hacspec</a><br></span></div></blockquote></div><br></div></div><br>______________________________<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" rel="noreferrer" target="_blank">https://moderncrypto.org/mailm<wbr>an/listinfo/hacspec</a><br>
<br></blockquote></span></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>