[hacspec] hacspec syntax

[Bryan Parno]

This seems like an excellent initiative — thanks for getting it going!  

I’ll have to take a closer look at the examples, but I had a quick question: in the language description (https://github.com/HACS-workshop/hacspec/blob/master/LANGUAGE.md <https://github.com/HACS-workshop/hacspec/blob/master/LANGUAGE.md>), why is `bytes` a special type, rather than being an array of uint8?  

Thanks,
-Bryan

> On Feb 10, 2018, at 8:16 AM, Karthikeyan Bhargavan <karthik.bhargavan at gmail.com> wrote:
> 
> Hello All,
> 
> It would be great to get some opinions on the hacspec syntax, types, and semantics.
> 
> At HACS, we started with cryptol as the initial language (which makes great sense considering the tool support.)
> On the hackathon day, the group moved towards a subset of python, since developers/spec authors already use it as pseudocode in RFCs.
> 
> For now, we have identified a small subset of python, with static types checked with mypy.
> We have written some specs in this subset in /specs and we believe this subset is adequate to write idiomatic specifications for most of the primitives currently in /formal-models.
> I believe this syntax can be compiled to idiomatic Cryptol and F*, but we need to see how they translate to other formalisms.
> 
> As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:
> 
> INTEGERS:
> 	The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)
> 	Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.
> TUPLES (RECORDS?):
> 	You can build and pass around tuples of values (Tuple[T1,…,Tn])
> 	We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)
> ARRAYS:
> 	The only other data structures currently are arrays of fixed-length (array[T]).
> 	You can read and write arrays, and you can read and write slices from arrays.
> 	You can filter an array or apply a function to each element using array comprehensions (like in Python).
> 	You can split an array into blocks and you can concatenate these blocks back into a flat array.
> 	We are uncertain whether to include higher-order operators like map and reduce or to rely on comprehensions and for-loops instead
> LOOPS:
> 	The only looping construct is a for loop over a range.
> 	If need be, we can add other looping constructs or recursion.
> SIDE-EFFECTS (?):
> 	Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.
> 	Functions always return their outputs, they do not modify any of their arguments.
> 	When arrays are passed into and out of functions, they are effectively copied in and copied out.
> 	This part of the semantics needs some thinking and discussion to find a good middle-ground,
> 	since the python syntax is naturally imperative, but most of the formal models we have looked
> 	at find it easier to reason about purely functional specificaion.
> 
> I am sure there is much else to look at and think about, but comments on the above would already be a good start.
> 
> Best regards,
> Karthik
> 
> 
> 
> 
> _______________________________________________
> 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/20180211/5223ba67/attachment.html>