[hacspec] hacspec syntax

[Franziskus Kiefer]

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.

Adam, do you want to update your PR to leave the other versions in so we
can compare all three of them?

On Sun, Feb 18, 2018 at 8:25 AM, Ben Laurie <benl at google.com> wrote:

>
>
> 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
>>
>>
>
> _______________________________________________
> 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/20180226/cf6e8163/attachment.html>