At IOHK, we are proud of our scientific approach and close collaboration with academia. We publish in peer reviewed scientific journals and present our results at acclaimed international conferences to ensure that our protocols and algorithms are built on rock-solid foundations. Our software must reflect this scientific excellence and quality, which means that we need a process to go from scientific results to actual code written in the Haskell programming language. We therefore decided to run internal training on “functional correctness”, so that the quality of our theoretical foundations can translate into equal quality for our code. We ran the first course over four days in Regensburg, Germany, two weeks ago. This training is aimed at everybody writing Haskell at IOHK, so we decided to run four sessions, roughly based on geography – there are IOHK engineers in 16 countries. We plan to do a second session in Regensburg in November and then two more early next year in the US. The lecturers were Andres Löh, co-founder of the Well-Typed consultancy, and John Hughes, the founder of QuviQ, who are both prominent in the Haskell world.

John is one of the creators of Haskell and the co-inventor of QuickCheck, the Haskell testing tool. Most mainstream software companies (if they do testing at all, which, sadly, is not always the case), use unit tests. For this, developers write down a number of tests by hand, cases that they deem typical or relevant or interesting, and then use a unit test framework to run the tests and report whether they yield the expected results. QuickCheck is different. Instead of specifying a handful of tests, developers using QuickCheck state the properties that their code should have. QuickCheck then generates many random test cases and checks the property for each of these. If QuickCheck finds that a property is violated, it first tries to simplify the test, then reports the simplest failing case back to the user.

As a simple example, let’s say you wrote a program to sort a list of names. Using unit tests, you would check the program against a few handcrafted examples of lists of names (something like "Tom", "Dick", "Harry" and "Dora", "Caesar", "Berta", "Anton" ). With QuickCheck, on the other hand, you would sit down and carefully think about properties your program should have In the example of sorting lists of names, what properties would you expect? Well, after running the program, you should get a list that is sorted alphabetically. Oh, and that list should contain all the names you entered. And yes, it should only contain those names you entered. You can write down these properties as Haskell programs, then hand them over to QuickCheck. The tool checks your properties against as many randomly generated lists of names as you wish (usually hundreds or thousands) and identifies any violations.

In practice, QuickCheck often manages to find problems that are overlooked by less rigorous methods, because their authors tend to overlook obscure cases and complicated scenarios. In our example, they may, for example, forget to test an empty list of names. Or there may be a bug in the program that only occurs for long lists of names, and their unit tests only check short lists. John had many ‘war stories’ of this happening in real life with real customers, where bugs were only revealed after a series of complex interleaved operations that no human unit test writer would have imagined.

Every Haskell developer has heard of QuickCheck and understands the basic ideas, but in complex real-world programs like Cardano, it is sometimes not so easy to use the tool properly. It was therefore great to have the intricacies and finer points explained by John himself, who has been using QuickCheck for 20 years and has worked with many industries, including web services (Riak, Dropbox and LevelDB), chat servers (Ejabberd), online purchasing (Dets), automotive (Autosar specification), and telecommunications (MediaProxy, Ericsson and Motorola). He helps find bugs and guarantee correctness every day. Given John’s experience, the training participants were able to spend about half of their time learning the finer points of QuickCheck from the master himself. It was tremendous fun enjoying John’s obvious enthusiasm for, and deep knowledge of, the subject. The rest of the session was dedicated to understanding the link between formal specifications, written in a mathematical style, and Haskell implementations.

At IOHK, we work very hard on writing correct code. For example, we specify program behavior and properties using rigorous mathematics. In the end, of course, we can’t deploy mathematics to a computer. Instead, our developers have to take the specification, translate the mathematics into Haskell and produce executable, efficient code. This process is easier for Haskell, because it is firmly rooted in mathematical principles, than for most languages, but it is still a conceptual leap. The specification talks about mathematical objects like sets and relations, which have to be translated into data types and functions as faithfully as possible. Nobody wins if your beautiful mathematics is ‘lost in translation’ and you end up with bug-ridden code. For example, when mathematicians talk about integers (..., −2, −1, 0, 1, 2,...) or real numbers (such as π, and √2), how do you express this in Haskell? There are data types like Int or Double that seem related, but they are not the same as the mathematical concepts they were inspired by. For example, a computer Int can overflow, and a Double can have rounding errors. It is important to understand such limitations when translating from mathematics to code. This is where the mathematician and renowned Haskell expert Andres Löh came in. He taught the participants how to read mathematical notation, how mathematical concepts relate to Haskell and how to translate from the one to the other.

For example, Andres presented the first pages of our formal blockchain specification and talked the participants through understanding and implementing this piece of mathematics as simple (and correct!) Haskell code, which led to interesting questions and lively discussions: How do you represent hashing and other cryptographic primitives? What level of detail do you need? Is it more important to stay as faithful to the mathematics as possible or to write efficient code? When should you sacrifice mathematical precision for simplicity?

In addition to their great lectures, John and Andres also provided challenging practical exercises, where participants could immediately apply their newly-gained knowledge about testing and specifications. Finally, there was plenty of opportunity for discussions, questions and socializing. Regensburg is a beautiful town, founded by the Romans two thousand years ago and a Unesco World Heritage Site. The city offered participants a perfect setting to relax after the training, continuing their discussions while exploring the medieval architecture or sitting down for some excellent Bavarian food and beer.

Artwork,

Mike Beeple

The IOHK Haskell and Cryptocurrency course in Barbados brought together students and professionals who were interested in learning the Haskell programming language. The course ran for eight weeks at the University of West Indies. Barbados was the second time the programme was offered, after a successful inaugural course held in Athens last year. The goal of the course is to extend the computer science training of participants and introduce them to Haskell, an elegant functional programming language, in the context of the cryptocurrency industry. Haskell is the language used in the Cardano cryptocurrency, and it was chosen because of the security benefits it offers.

The course was designed and taught by Haskell and functional programming experts, including myself, and Dr. Andres Löh of Well Typed and Dr. Marcin Szamotulski, Haskell Developer at IOHK. Visiting lecturers included Prof. Philip Wadler, one of the creators of Haskell, and IOHK Area Leader in Programming Languages, and Cardano SL developer, Darryl McAdams. The instructors aimed to strike a balance between theory and practice, teaching the students both theoretical background of functional programming in Haskell in particular (Lambda Calculus, System F, Category Theory, etc), but also introducing them to popular libraries and important techniques for solving real-world problems (networking, parsing, resource handling, and more). At the end of each course, students are given the opportunity to apply for positions at IOHK and continue their professional career in Haskell.

Here are the stories of two students who attended the IOHK Haskell and Cryptocurrency course in Barbados:

Jordan Millar - Jordan is currently a chemist with an M.Sc. in organic chemistry from Oxford University.

Upon hearing that IOHK was offering a free Haskell and Cryptocurrency course in Barbados I decided it would be foolish to not enroll. The stars aligned for me as Barbados is a stone’s throw away from Trinidad and Tobago, my home, and I was acutely aware of IOHK’s approach to cryptocurrency.

My programming experience prior to this course was limited; I predominantly had written scripts in Python over the last two years. Only a few weeks prior to the course, I had become interested in Haskell through a functional programmer I happened to meet.

IOHK piqued my curiosity because at the time, they were the only company in the cryptocurrency space driven by research. This resonated with me as I had first-hand experience with research and development, albeit in a different field. I work in organic chemistry, and am currently working with a cleaning product manufacturer on their formulations. I appreciate the importance of developing a model, trying to break it yourself, and then having people smarter than you also trying to break it. In particular, if these networks are destined to hold hundreds of billions of dollars, you cannot afford to construct these networks in the ad hoc manner we have often seen before. With this in mind, I set off to Barbados to learn more about Haskell and IOHK’s methodology.

The course was a whirlwind tour of Haskell starting with data types all the way to type families and everything in between. We charged through a series of topics and on a weekly basis were given a problem sheet to complete. Dr. Lars Brünjes and Dr. Marcin Szamotulski were exceptional teachers. They delivered the content effectively and gave additional clarification when required.

The course was challenging, especially because I had missed the first week due to logistical issues. That being said, I came to find that Haskell is an elegant and concise programming language. IOHK flew Philip Wadler to Barbados to give a couple of lectures! What stood out to me the most was his demonstration of the Curry-Howard correspondence. It was fascinating to see the link between mathematical proofs and programs. IOHK’s Darryl McAdams also visited us in Barbados and took us through compilers in Haskell. The elegance of Haskell really shone here in my opinion as she effortlessly created a simply typed programming language during class.

It wasn’t all work and no play; IOHK sponsored many dinners and outings while we were in Barbados. This rounded off the course nicely as everybody had time to socialize outside of the classroom. To top it off, Charles Hoskinson took time out of his incredibly busy schedule to come and see us in Barbados. Having only seen Charles in YouTube videos, it was a privilege to hear him share his future plans and vision for IOHK in person. If you thought his conviction transmitted effectively through his interviews online, wait until you hear him in person.

All in all, it was a great experience. To anybody reading this, I highly recommend enrolling in this course if you get the chance to!

Rob Cohen - Rob divides his time between his information security consulting firm Callidus Security and serving in the cyber security field in the US military. He graduated from Columbia University in 2015 with a BA in Computer Science and Mathematics.

I was fortunate to be invited to attend IOHK's eight-week course, "Haskell and Cryptocurrency" in Barbados in early 2018. Prior to the course, my only experience with functional programming had been in a Compilers course I had taken in college and some toy projects I had built as experiments. As a result I knew this course would be challenging, and it turned out to be exactly the kind of deep-dive crash course on Haskell and functional programming that I was hoping for. This course was demanding, requiring dedication in the classroom and diligence in applying those concepts in our assigned homeworks and group projects.

The course covered a variety of topics, from the basics of IO and higher-order functions, to lambda calculus, optics, free monads, GADTS and Generic Programming concepts (and much more). Beyond the theory, what I found most rewarding in the course was working with my fellow classmates on our group projects. One project my team worked on involved building the early stages of a working Bitcoin client in Haskell! Working on larger-scale projects like that really helped Haskell come alive for me. Furthermore, guest lectures by Phil Wadler and Darryl McAdams from IOHK's Plutus team were pleasant surprises as well.

This course was not easy; there were times where I really felt my mettle was challenged. However, I stuck with it and pushed through. Now I not only have a deeper understanding and appreciation of the theoretical underpinnings of Haskell, but I came out as a developer with a stronger constitution as well. I am grateful to Lars and Marcin (the course instructor and teacher assistant) for all their hard work on the course. They put a tremendous amount of effort into the course materials and it showed. There were frequently times where their diagrams and explanations were better than Haskell's own official documentation!

The highlight of the course was the opportunity to work closely with such incredible developers from all around the world. My classmates hailed from Japan, Ireland, Argentina, Poland, Germany, Sweden, the USA, and the Caribbean. It was truly remarkable to have so many people from all over the world working together in one room trying to figure out how to learn Haskell. To my fellow classmates, I am deeply grateful for your support and camaraderie during the course. I salute you all for your dedication and hard work. I also look forward to our (spearfishing) reunion someday!

I can safely say that I've been bitten by the Haskell bug, and I look forward to being a member of the Haskell/functional programming community for years to come. I highly recommend this course to anyone who is interested in learning about Haskell and functional programming.

Why do we need transaction fees?

There are two main reasons why transaction fees are needed for a cryptocurrency like Cardano:

People who run full Cardano nodes spend time, money and effort to run the protocol, for which they should be compensated and rewarded. In contrast to Bitcoin, where new currency is created with each mined block, in Cardano, transaction fees are the only source of income for participants in the protocol.

The second reason for transaction fees is the prevention of DDoS (Distributed Denial of Service) attacks. In a DDoS attack, an attacker tries to flood the network with dummy transactions, and if he has to pay a sufficiently high fee for each of those dummy transactions, this form of attack will become prohibitively expensive for him.

How do transaction fees work?

Whenever somebody wants to transfer an amount of Ada, some minimal fees are computed for that transaction. In order for the transaction to be valid, these minimal fees have to be included (although the sender is free to pay higher fees if he so wishes). All transaction fees are collected in a virtual pool and then later distributed amongst participants in the Cardano protocol.

How are the minimal transaction fees calculated?

The minimal fees for a transaction are calculated according to the formula

a + b × size,

where 'a' and 'b' are constants and 'size' is the size of the transaction in Bytes. At the moment, the constants 'a' and 'b' have the values

a = 0.155381 ADA,
b = 0.000043946 ADA/Byte.

This means that each transaction costs at least 0.155381 ADA, with an additional cost of 0.000043946 ADA per Byte of transaction size. For example, a transaction of size 200 Byte (a fairly typical size) costs

0.155381 ADA + 0.000043946 ADA/Byte × 200 Byte = 0.1641702 ADA.

Why did we pick this particular formula? The reason for having parameter 'a' is the prevention of DDoS attacks mentioned above: even a very small dummy transaction should cost enough to hurt an attacker who tries to generate many thousands of them. Parameter 'b' has been introduced to reflect actual costs: storing larger transactions needs more computer memory than storing smaller transactions, so larger transactions should be more expensive than smaller ones.

In order to arrive at the particular values for parameters 'a' and 'b', we had to answer questions like:

• How expensive is one byte of computer memory?
• How many transactions will there be on average per second?
• How large will a transaction be on average?
• How much does it cost to run a full node?

We had to estimate the answers to those questions, but now that Cardano is up and running, we will be able to gather statistics to find more accurate answers. This means that 'a' and 'b' will probably be adjusted in future to better reflect actual costs.

We even plan to eventually come up with a scheme that will adjust those constants dynamically in a market driven way, so that no human intervention will be needed to react to changes in traffic and operational costs. How to achieve this is one focus of our active research.

How are fees distributed?

All transaction fees of a given "epoch" are collected in a virtual pool, and the idea is to then redistribute the money from that pool amongst people who were elected "slot leaders" by the proof of stake algorithm during that epoch and who created blocks.

At this stage of Cardano, where all blocks are created by nodes operated by IOHK and our partners, fees are already collected (to prevent DDoS attacks), but they will not be distributed and instead will be burnt.

As soon as Cardano enters its next, fully decentralized stage, fees will be distributed as described above.

What next?

Coming up with a solid scheme for fee distribution is a challenging mathematical problem: How do we incentivize "good" behavior and promote efficiency while punishing "bad" behavior and attacks? How do we make sure that people who participate in the protocol receive their fair reward, while also ensuring that the best way to earn money with Cardano is to make the system as reliable and efficient as possible? The trick is to align incentives for node operators with the "common good", so that rewards are highest when the system is running at optimal performance.

These are questions studied by the mathematical discipline called Game Theory, and we are proud to have prominent game theorist and Gödel Award laureate Prof. Elias Koutsoupias of the University of Oxford working with us on finding solutions to this problem.