Q: I heard there aren't many programmers able to code in f* isn't that one of the biggest problems for Zen Protocol right now? (12/6/18 telegram)


#1

(By Asher Manning): There were no programmers able to code in Bitcoin Script when Bitcoin came out, no programmers able to code in Solidity when Ethereum came out…

Solidity caught on somewhat because it’s fairly similar in syntax to the ‘C-like’ languages, eg. Java, Javascript, C++, C#, etc. The Ethereum founders weren’t sure what exactly Ethereum would be used for, and so they chose to create a language similar to popular general-purpose languages so that the barrier to entry would be lowered somewhat.

In the financial sector, ‘functional’ languages are pervasive. These would be languages like F#, OCaml, Haskell, and Scala - as an example, these are respectively used by SIG, Jane Street, Standard Chartered, and Morgan Stanley. Functional languages are used in finance because they offer high security/stability, high performance, and low development time. They have the drawback that they are somewhat exotic - they are very different from other languages. Despite this, they are usually quite simple - Functional languages are also strongly preferred in programming language research because of their simplicity. This simplicity is also what makes functional languages ‘easy’ to reason about(as in, formal verification), although most practical languages are not capable of formal verification - F* is rather unique in this regard.

Zen Protocol’s goal is to become a financial platform, and so it’s important to have tools that are relevant to the developers that we wish to attract. F* should be fairly familiar to users of F#, OCaml, and Haskell (F* is actually a dialect of F# and OCaml) and somewhat familiar for Scala developers.

Zen’s paradigm or resource bounded computation only works for languages that are capable of expressing resource bounds (reliably) anyway. For reference, that would be F*, Coq, Agda, and a few research languages that only exist on paper. Coq and Agda are proof assistants, they are not designed for writing programs and are comparatively awkward to use. Of course I’m aware that it’s an unusual decision to work with an exotic language, but the decision was the result of very careful deliberation, and all things considered I’m confident that it was the correct choice.