[hacspec] hacspec syntax

Ben Laurie benl at google.com
Sat Feb 17 23:25:20 PST 2018


On 17 February 2018 at 23:36, Karthikeyan Bhargavan <
karthik.bhargavan at gmail.com> wrote:

> Looks nice.
>
> I’ve been wondering about how to balance between higher-order functions,
> generator/list comprehension syntax, and standard imperative loops.
> 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.
> Are comprehensions a good middle-ground? Are they even more confusing to
> programmers?
>

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.

Of course, they are less flexible than loops. :-)


>
> -Karthik
>
> On 17 Feb 2018, at 23:04, Adam Chlipala <adamc at csail.mit.edu> wrote:
>
> One small suggestion for Poly1305: I've created a PR
> <https://github.com/HACS-workshop/hacspec/pull/6> that redoes polynomial
> evaluation with comprehensions, in a different way.  I expect this version
> should be easier to translate to backends we care about.
>
> What do you think?
> _______________________________________________
> Hacspec mailing list
> Hacspec at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/hacspec
>
>
>
> _______________________________________________
> Hacspec mailing list
> Hacspec at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/hacspec
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180218/11069b14/attachment.html>


More information about the Hacspec mailing list