[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