<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">This seems like an excellent initiative — thanks for getting it going! </div><div class=""><br class=""></div><div class="">I’ll have to take a closer look at the examples, but I had a quick question: in the language description (<a href="https://github.com/HACS-workshop/hacspec/blob/master/LANGUAGE.md" class="">https://github.com/HACS-workshop/hacspec/blob/master/LANGUAGE.md</a>), why is `bytes` a special type, rather than being an array of uint8? </div><br class=""><div class=""> <div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;">Thanks,<br class="">-Bryan<br class=""></div> </div> <div><br class=""><blockquote type="cite" class=""><div class="">On Feb 10, 2018, at 8:16 AM, Karthikeyan Bhargavan <<a href="mailto:karthik.bhargavan@gmail.com" class="">karthik.bhargavan@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Hello All,<br class=""><br class="">It would be great to get some opinions on the hacspec syntax, types, and semantics.<br class=""><br class="">At HACS, we started with cryptol as the initial language (which makes great sense considering the tool support.)<br class="">On the hackathon day, the group moved towards a subset of python, since developers/spec authors already use it as pseudocode in RFCs.<br class=""><br class="">For now, we have identified a small subset of python, with static types checked with mypy.<br class="">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.<br class="">I believe this syntax can be compiled to idiomatic Cryptol and F*, but we need to see how they translate to other formalisms.<br class=""><br class="">As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:<br class=""><br class="">INTEGERS:<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.<br class="">TUPLES (RECORDS?):<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>You can build and pass around tuples of values (Tuple[T1,…,Tn])<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)<br class="">ARRAYS:<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>The only other data structures currently are arrays of fixed-length (array[T]).<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>You can read and write arrays, and you can read and write slices from arrays.<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>You can filter an array or apply a function to each element using array comprehensions (like in Python).<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>You can split an array into blocks and you can concatenate these blocks back into a flat array.<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>We are uncertain whether to include higher-order operators like map and reduce or to rely on comprehensions and for-loops instead<br class="">LOOPS:<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>The only looping construct is a for loop over a range.<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>If need be, we can add other looping constructs or recursion.<br class="">SIDE-EFFECTS (?):<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Functions always return their outputs, they do not modify any of their arguments.<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>When arrays are passed into and out of functions, they are effectively copied in and copied out.<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>This part of the semantics needs some thinking and discussion to find a good middle-ground,<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>since the python syntax is naturally imperative, but most of the formal models we have looked<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>at find it easier to reason about purely functional specificaion.<br class=""><br class="">I am sure there is much else to look at and think about, but comments on the above would already be a good start.<br class=""><br class="">Best regards,<br class="">Karthik<br class=""><br class=""><br class=""><br class=""><br class="">_______________________________________________<br class="">Hacspec mailing list<br class=""><a href="mailto:Hacspec@moderncrypto.org" class="">Hacspec@moderncrypto.org</a><br class="">https://moderncrypto.org/mailman/listinfo/hacspec<br class=""></div></div></blockquote></div><br class=""></body></html>