Pact: An Open Source Language for Smart Contracts
In this talk we'll discuss the design and implementation of a smart contract property verification tool for Pact.
The revolutionary idea of putting computer programs in a blockchain to create smart contracts has opened up a whole new world of possibilities. But these programs have very different characteristics from other software. This talk explores these differences, some of the challenges that have been encountered, and then discusses how Kadena is solving these problems with its smart contract language Pact. We'll discuss the design and implementation of a smart contract property verification tool for Pact. We leverage these (lack of) features to build a system capable of proving many properties of contracts via the Z3 SMT solver. We'll also give examples of real bugs caught by the system.
Outline/Structure of the Demonstration
In this talk we'll discuss the design and implementation of a smart contract property verification tool for Pact, as well as the Pact language properties itself, all written in Haskell.
Additionally, we will discuss the Z3 SMT Solver, and how this was incorporated into Pact as a means of proving properties of smart contracts.
We will then discuss the class of bugs caught by this infrastructure.
Learning Outcome
Attendees will leave with an understanding of Kadena.io's Pact Smart Contract language, its implementation (in Haskell), as well as some interesting results in proving properties with Z3.
Target Audience
Blockchain users, Haskell users, PLT enthusiasts
Prerequisites for Attendees
None
Links
http://kadena.io/docs/Kadena-PactWhitepaper.pdf
http://pact-language.readthedocs.io/en/latest/pact-reference.html
https://github.com/kadena-io/pact
schedule Submitted 2 years ago
People who liked this proposal, also liked:
-
keyboard_arrow_down
Michael Snoyman - Functional Programming for the Long Haul
45 Mins
Keynote
Beginner
How do you decide whether a programming language is worth using or not? By necessity, such decisions are usually based on assessments that can be made relatively quickly: the ease of using the language, how productive you feel in the first week, and so on. Unfortunately, this tells us very little about the costs involved in continuing to maintain a project past that initial phase. And in reality, the vast majority of time spent on most projects is spent in those later phases.
I'm going to claim, based on my own experience and analysis of language features, that functional programming in general, and Haskell in particular, are well suited for improving this long tail of projects. We need languages and programming techniques that allow broad codebase refactorings, significant requirements changes, improving performance in hotspots of the code, and reduced debug time. I believe Haskell checks these boxes.
-
keyboard_arrow_down
Aaron W Hsu - Does APL Need a Type System?
45 Mins
Talk
Intermediate
APL is known for its concise problem-solving expressiveness, and it is used very successfully in places where high-quality and rapid iteration are requirements, not luxuries. Static Type Systems have had tremendous success throughout the computing industry, even receiving positive HCI usability studies that demonstrate their effectiveness on a number of metrics with mainstream and functionally-oriented programming languages. This success leads many programmers to take the value of type systems as a given, especially as mission-criticality and the age of a project increase. Therefore, it comes as a surprise to many, when learning about APL, that it has spent so long as an untyped, interpreted language in domains and use cases where traditional wisdom would suggest the need for a typed, compiled language.
But APL is not like other languages, and its unique features and historical uses warrant a careful revisiting of the question of type systems. In this talk we will explore whether or not APL needs a type system, whether it would benefit from having one, what that might look like, and how the interaction between APL and type theory might inform the design and use of type systems in general.
-
keyboard_arrow_down
Anne Ogborn - Declarative Expressions of Behavior
45 Mins
Talk
Beginner
We write programs in a different language than we talk about them. "So we get a request, do the security mumble, pass it to the middleware that grabs ..."
Can we get closer to writing programs that describe the program's desired behavior? And why do such attempts always get poo-pooed by programmers?
This is a foofy cloud shaped drawings exploration of other ways to express software design intent, mostly by cheating.
-
keyboard_arrow_down
Saurabh Nanda - "Refresh-driven" development with Haskell & Elm
45 Mins
Tutorial
Beginner
We sorely missed the rapid "refresh-based" feedback loop available in Rails (and other dynamically typed web frameworks), while writing Haskell. Change your code, hit save, and refresh your browser!
In this talk we will share a few tips on how we finally hit productivity nirvana with ghcid and automated code-gen.
Best of both worlds -- rock-solid type-safety AND being able to reload code with every change.
-
keyboard_arrow_down
Sudipta Mukherjee - Creating DSLs in functional Kotlin
45 Mins
Demonstration
Intermediate
Domain Specific Languages (or Libraries because embedded DSLs are just that) are already quite popular.
Modern languages have many useful language features that are conducive to create DSLs with more ease than ever before. Kotlin from JetBrains is a beautifully blended pragmatic programming language that packages many features from many programming languages. Kotlin also have infix operation which makes code written in a DSL made with Kotlin very easy to read (and therefore less error-prone).
In this demonstration, I shall show couple DSLs made from Kotlin
and will dissect the code LIVE to show audience how several language features in Kotlin (which sometimes requires playing with higher order functions) to develop these languages.
*A Unit Testing DSL (a DSL to simplify unit testing of Kotlin, Java Code) that our grand/m/pa can use.
-- All unit test frameworks serve the purpose but elegance is a different matter. A code that works, and a code that is elegant and works is art. In this example, audience will see how they can use several language features that Kotlin has to offer can be put together to create an elegant and expandable unit testing DSL.
* A DSL for Web Scraping and Transformation.
- - A special case of ETL, where Extraction happens from raw HTML, Transformation happens in memory using the DSL designed. and the Load happens by loading this data to a different schema/db/form/representation.
-
keyboard_arrow_down
Raghu Ugare / Vijay Anant - (Why) Should You know Category Theory ?
Raghu UgareArchitect, Designer, DeveloperLambdaMattersVijay AnantArchitect, Designer, DeveloperLambdaMattersschedule 2 years ago
45 Mins
Talk
Intermediate
Category Theory has been found to have a vast field of applications not limited to programming alone.
In this fun-filled talk (Yes! We promise!) , we want to make the audience fall in love with Math & Category Theory in general, and Haskell in particular.
We will address questions such as below:- What is the mysterious link between the abstract mathematical field of Category Theory and the concrete world of real-world Programming ? And why is it relevant especially in Functional Programming?
- Most of all, how can You benefit knowing Category Theory ? (Examples in Haskell)
-
keyboard_arrow_down
Harendra Kumar - High Performance Haskell
45 Mins
Talk
Intermediate
Haskell can and does perform as well as C, sometimes even better. However,
writing high performance software in Haskell is often challenging especially
because performance is sensitive to strictness, inlining and specialization.
This talk focuses on how to write high performance code using Haskell. It is
derived from practical experience writing high performance Haskell libraries. We
will go over some of the experiences from optimizing the "unicode-transforms"
library whose performance rivals the best C library for unicode normalization.
From more recent past, we will go over some learnings from optimizing and
benchmarking "streamly", a high performance concurrent streaming library. We
will discuss systematic approach towards performances improvement, pitfalls and
the tools of the trade. -
keyboard_arrow_down
Tony Morris - Parametricity, Functional Programming, Types
45 Mins
Talk
Intermediate
In this talk, we define the principle of functional programming, then go into
detail about what becomes possible by following this principle. In particular,
parametricity (Wadler, 1989) and exploiting types in API design are an essential
property of productive software teams, especially teams composed of volunteers
as in open-source. This will be demonstrated.Some of our most important programming tools are neglected, often argued away
under a false compromise. Why then, are functional programming and associated
consequences such as parametricity so casually disregarded? Are they truly so
unimportant? In this talk, these questions are answered thoroughly and without
compromise.We will define the principle of functional programming, then go into
detail about common problems to all of software development. We will build the
case from ground up and finish with detailed practical demonstration of a
solution to these problems. The audience should expect to walk away with a
principled understanding and vocabulary of why functional programming and
associated techniques have become necessary to software development. -
keyboard_arrow_down
Michael Ho - Making the Switch: How We Transitioned from Java to Haskell
45 Mins
Case Study
Intermediate
In this case study presentation, SumAll's CTO, Todd Sundsted, and Senior Software Engineer, Michael Ho, will discuss the move from Java to Haskell along two parallel paths. First, the business/political story — how SumAll convinced the decision makers, fought the nay-sayers, and generally managed the people impacted by the transition. Second, the technical story — how they actually replaced their Java code with Haskell code. Along the way, they will address their hopes and expectations from transitioning from Java to Haskell, and will conclude with the results they've gained and seen to date.
-
keyboard_arrow_down
Anupam Jain - Purely Functional User Interfaces that Scale
45 Mins
Talk
Beginner
A virtual cottage industry has sprung up around Purely functional UI development, with many available libraries that are essentially just variants on two distinct approaches: Functional Reactive Programming (FRP), and some form of functional views like "The Elm Architecture". After having worked extensively with each of them, I have found that none of the approaches scale with program complexity. Either they are too difficult for beginners trying to build a hello world app, or they have unpredictable complexity curves with some simple refactorings becoming unmanageably complex, or they "tackle" the scaling problem by restricting developers to a safe subset of FP which becomes painful for experienced developers who start hitting the complexity ceiling.
In this talk I give an overview of the current Purely Functional UI Development Landscape, and then present "Concur", a rather unusual UI framework, that I built to address the shortcomings of the existing approaches. In particular, it completely separates monoidal composition in "space" (i.e. on the UI screen), from composition in "time" (i.e. state transitions), which leads to several benefits. It's also a general purpose approach, with Haskell and Purescript implementations available currently, and can be used to build user interfaces for the web or for native platforms.
The biggest advantage of Concur that has emerged is its consistent UI development experience that scales linearly with program complexity. Simple things are easy, complex things are just as complex as the problem itself, no more. Reusing existing widgets, and refactoring existing code is easy and predictable. This means that Concur is suitable for all levels of experience.
- For Learners - Concur provides a consistent set of tools which can be combined in predictable ways to accomplish any level of functionality. Due to its extremely gentle learning curve, Concur is well suited for learners of functional programming (replacing console applications for learners).
- For experienced folks - Assuming you are already familiar with functional programming, Concur will provide a satisfying development experience. Concur does not artificially constrain you in any form. You are encouraged to use your FP bag of tricks in predictable ways, and you are never going against the grain. It's a library in spirit, rather than a framework.
-
keyboard_arrow_down
Michael Snoyman - Applied Haskell Workshop
480 Mins
Workshop
Intermediate
This full day workshop will focus on applying Haskell to normal, everyday programming. We'll be focusing on getting comfortable with common tasks, libraries, and paradigms, including:
- Understanding strictness, laziness, and evaluation
- Data structures
- Structuring applications
- Concurrency and mutability
- Library recommendations
By the end of the workshop, you should feel confident in working on production Haskell codebases. While we obviously cannot cover all topics in Haskell in one day, the goal is to empower attendees with sufficient knowledge to continue developing their Haskell skillset through writing real applications.
-
keyboard_arrow_down
Brian McKenna - Starting Data61 Functional Programming Course
90 Mins
Workshop
Beginner
Following Tony and Alois' Introduction to Haskell syntax and tools, we will work through the first few modules of Data61's Functional Programming Course. These modules cover writing functions for the optional and list data types.
We will complete enough exercises to cover basic data types, functions and polymorphism. We'll practice the techniques of equational reasoning, parametricity and type/hole driven development. After completing these modules, you should be able to use the techniques to attempt most other exercises in the repository.
This workshop has the same requirements as Tony's introduction, along with a download of a recent version of the fp-course repository (https://github.com/data61/fp-course).
-
keyboard_arrow_down
Luka Jacobowitz - Testing in the world of Functional Programming
45 Mins
Demonstration
Intermediate
Testing is one of the most fundamental aspects of being a software developer. There are several movements and communities based on different methodologies with regards to testing such as TDD, BDD or design by contract. However, in the FP community testing is often not a large topic and is often glossed over. While it’s true that testing in functional programming tends to be less important, there should still be more resources on how to create tests that add actual value.
This talks aims to provide exactly that, with good examples on how to leverage property based testing, refinement types and the most difficult part: figuring out how to test code that interacts with the outside world.
-
keyboard_arrow_down
Tony Morris - Let's Lens
480 Mins
Workshop
Intermediate
Let's Lens presents a series of exercises, in a similar format to the Data61 functional programming course material. The subject of the exercises is around the concept of lenses, initially proposed by Foster et al., to solve the view-update problem of relational databases.
The theories around lenses have been advanced significantly in recent years, resulting in a library, implemented in Haskell, called lens.
This workshop will take you through the basic definition of the lens data structure and its related structures such as traversals and prisms. Following this we implement some of the low-level lens library, then go on to discuss and solve a practical problem that uses all of these structures.
-
keyboard_arrow_down
Markus Hauck - Free All The Things!
45 Mins
Talk
Intermediate
Have you ever asked yourself why we only free monads? Turns out there are a lot of other structures that want to be liberated from the constraints of their existence! In this talk, we will investigate what other poor (algebraic) structures we can free from the dirty hands of imperative programmers. Our journey starts with the well-known free monads, but after that we will have a look at all the other interesting structures that can be freed and of course we will also look at what we can do with them.
-
keyboard_arrow_down
Brian McKenna - Eta and Nix for shipping Haskell to Java environments
20 Mins
Demonstration
Beginner
Eta compiles Haskell code to Java/JVM bytecode. It supplies a Foreign Function Interface for interoperating with Java code. Many existing Haskell libraries (e.g. lens, Servant, QuickCheck) are ported to Eta so it's possible to use them for many traditionally Java environments, including Amazon Lambda functions, Kinesis consumers and Spark jobs.
The Nix expression language allows writing functions to specify builds. The Nix build tool takes these expressions and instantiates them into static build instructions. These instructions can then be realised and turned into outputs. At each step Nix' tooling provides a layer of purity.
Using Eta and Nix together, we can use Haskell functions for applications and Nix functions for builds, then deploy them to Java environments!
-
keyboard_arrow_down
Emily Pillmore - A Radically New Functional Blockchain Architecture: Chainweb
45 Mins
Talk
Advanced
Proof-of-work blockchain networks like Bitcoin, Litecoin and Ethereum are characterized by low throughput (5-15 transactions per second). Efforts to improve throughput through protocol modifications, such as block size increases, have no hope of reaching levels required to take on modern fiat-currency payment networks. However, efforts that seek to replace Proof-of-Work (Proof-of-Stake and variants) or integrate it with off-chain networks and processes (payment channels, side chains) degrade assurance, censorship resistance or trustless-ness of the original design. Recovering and elaborating on early proposals for Bitcoin scaling, we present ChainWeb, a parallel-chain architecture which can combine hundreds to thousands of Proof-of-Work blockchains pushing throughput to 10,000 transactions per second and beyond. The network transacts a single currency, using atomic and trustless SPV (Simple Payment Verification) cross-chain transfers orchestrated at the application layer with capability and coroutine support in the Pact smart contract language. Chains incorporate each other’s Merkle tree receipts to enforce a single “super branch” offering an effective hash power that is the sum of each individual chain’s hash rate. In addition to massive throughput, other benefits accrue from having a truly parallelized smart-contract blockchain system.
-
keyboard_arrow_down
Andrew McMiddlin - Property-based State Machine Testing
45 Mins
Talk
Intermediate
Automated testing is key to ensuring the ongoing health and well-being of any software project,giving developers and users confidence that their software works as intended. Property based testing is a significant step forward compared to traditional unit tests, exercising code with randomly generated inputs to ensure that key properties hold. However, both of these techniques tend to be used at the level of individual functions. Many important properties of an application only appear at a higher level, and depend on the state of the application under test. The Haskell library hedgehog, a relative newcomer to the property based testing world, includes facilities for property-based state machine testing, giving developers a foundation on which to build these more complicated tests.
In this talk, Andrew will give you an introduction to state machine property testing using hedgehog. He'll start with a quick refresher on property based testing, followed by a brief introduction to state machines and the sorts of applications they can be used to model. From there, he'll take you on a guided tour of hedgehog's state machine testing facilities. Finally, Andrew will present a series of examples to show off what you can do and hopefully give you enough ideas to start applying this tool to your own projects. The first set of examples will test a web application written in Haskell. These tests will include: content creation and deletion, uniqueness constraints, authentication, and concurrent transactions. A second set of examples will test an application written in a language other than Haskell to demonstrate that this technique is not limited to applications written in Haskell.
An intermediate knowledge of Haskell and familiarity with property based testing will be beneficial,but not essential. The slides and demo application will be available after the talk for people to study in detail.
-
keyboard_arrow_down
Neeraj Sharma - BeamParticle - A Polyglot Dynamic Programming Engine
90 Mins
Tutorial
Intermediate
BeamParticle is an open source project built on top of the Erlang virtual machine (BEAM), which allows dynamic (re)programming in multiple programming languages. This project tries to take some simple decisions thereby making the life of developer easy in realizing dynamic code patching and reprogrammability. It is very easy to setup this software on any of the modern GNU/Linux distributions, although Debian packages are available for Ubuntu Xenial. The project supports six different programming languages; namely: Erlang, Elixir, Java, Python, Efene, and PHP.
The system is deployed in a limited capacity in production within redBus to serve numerous use cases.
-
keyboard_arrow_down
Aloïs Cochard - The Magnum Opus
45 Mins
Talk
Beginner
From Ancient Egypt to the Middle Ages humanity lost it's way in the quest to find the philosopher's stone.
While following the recent advance in machine learning one might think that we are running in that same quest again,
only differences this time are that our philosopher's stone is deep learning and the promise is general artificial intelligence instead of immortality.The current machine learning ecosystem is mainly based on python and pretty much feels like alchemy,
lot of trial and errors, lack of tooling and good engineering practices, ...Let's take a tour of the current ecosystem and see how can we do better and safer high performance machine learning using Haskell!