[hacspec] hacspec syntax

Karthikeyan Bhargavan karthik.bhargavan at gmail.com
Sat Feb 17 15:36:57 PST 2018


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?

-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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180218/07ded882/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180218/07ded882/attachment.sig>


More information about the Hacspec mailing list