[Cryptography] ?crypto in fully functional style

[Henry Baker]

At 03:07 PM 9/14/2016, John Denker wrote:
>On 09/14/2016 10:00 AM, Henry Baker wrote:
>> Now that nearly all compilers utilize *pure functional* internal
>> representations of computations, and *variable assignments* have
>> been shown to be frighteningly expensive -- especially in a
>> multiprocessor world -- it's time to move to fully functional machine
>> languages
>
>To pursue that idea, I looked up some of implementations of AES and ChaCha in lisp.
>
>The first ones that I found (emacs and common lisp) were underwhelming, with lots of setf and setcar statements (like (fortran (with (parentheses)))).
>
>The story is similar with Haskell:
>
>It is touted as a "fully functional" language but it still has ByteArrays.
>
>Therefore, a question:
>
>Can anybody point to an implementation of some interesting crypto primitive, AES or ChaCha or whatever, written in a fully functional style?
>
>If not, is this a consequence of how the primitives are defined?
>
>Do we even know how to define a natively, inherently functional- style cipher?
>
>Should we have a contest to create one?
>
>For reference, some examples:
>
>https://github.com/Sauermann/emacs-aes/blob/master/aes.el
>
>https://github.com/froydnj/ironclad/blob/master/src/ciphers/chacha.lisp
>
>https://github.com/haskell-crypto/cryptonite/blob/master/Crypto/Cipher/AES/Primitive.hs

I've seen references to *Cryptol*, a domain-specific language for crypto.  However,
I don't know whether it would be considered "functional-style".

http://cryptol.net/documentation.html

http://cryptol.net/files/empowering_the_experts.pdf

It apparently can be compiled directly into an FPGA.