Skip navigation

Following is a report from CS doctoral student Andrew Marmaduke, working with me here at U. Iowa, on his attendance at DevCon4:

Devcon4 is the Ethereum developer conference that was hosted in Prague.  Thanks to my adviser Aaron Stump and the grant awarded to him by the Ethereum Foundation I was able to attend. Moreover, because I was representing The University of Iowa as a grantee, I also got to sit down in the Grantee Showcase and talk a little bit about Cedille with those who were interested. To start off, I’ll share my first impressions of Devcon4.

It would be a mistake, I think, not to mention the city of Prague when talking about a first impression.
Prague is a very beautiful city and the conference (held at Prague Conference Centre) was outside of Prague 1 (or the tourist hotspot). I spent every day walking to and from the conference. Honestly, it felt like any other major city, but the architecture was quite beautiful even outside of Prague.

Prague is known for its beer and I heard that there were no shortage of parties and drinking after a conference day ended. It felt informal in a good way. That’s my first stand out impression of Devcon4.
With idle chatter and friends reuniting or friendships sprouting it wasn’t all business or academics.
And have I mentioned the light show performance room? Every day during the conference there was a decompression room where a performer sitting in the center played several ethereal sounding instruments (like chimes, low frequency drums, etc) with a column of lights hanging above her and pillows and comfy carpets surrounding her. I know that the carpets were comfy because I spent an hour or two decompressing on the last day!

However, the conference also had a distinctly business feel.I’ve been to my fair share of academic conferences and have attend a developer conference or two before Devcon4, but I’ve never had an investor ask me for an elevator pitch.Needless to say, if you’re a researcher keen to network inside the blockchain business world then I would wager it’s worth your time to attend Devcon5.

Aside from first impressions I arrived at the conference with a particular skepticism about blockchain and the vision of Ethereum. I set a goal for myself to try and resolve that skepticism and to cut through the hype. I feel like I succeeded. Indeed, I now believe that the future is bright for some kind of cryptographically foundational technology that other solutions are built on top of, let’s talk briefly about why. Before we begin I want to make it clear that I am not a blockchain researcher and any speculation I offer should be taken with a grain of salt. First, there seems to be some significant problems inherent to a fully distributed model that is used in blockchain. Obviously, the Byzantine General’s problem is the principle issue that is addressed by Bitcoin and other blockchain solutions but Phil Daian gave a critical talk against Ethereum that highlighted that there is more to the story. Phil wrote his thoughts in a blogpost which may be an easier way to consume his ideas until the video recordings of the talks at Devcon4 are live [1]. To summarize, on-chain voting is a difficult and possibly impossible problem to solve without allowing for effective vote buying. Moreover, nefarious decentralized entities (named Dark DAOs by Phil) could pull resources and damage the stability of a blockchain.

The situation does not seem hopeful after reading Phil’s opinion on Ethereum! However, Vitalik Buterin a co-founder of Ethereum gave a roadmap talk about the future of Ethereum that alleviated some concerns. In his talk he discussed proof of stake, rent for long term storage, layer two solutions, and many other things, but the key take away for me was that Ethereum is willing to acknowledge and solve problems illuminated by people like Phil. For now the problems the developers at Ethereum have been trying to solve are scalability focused and the story for that is promising. In particular I would like to highlight the notion of “Layer 2”.

The idea behind Layer 2 is that you can sacrifice some properties given to you by the blockchain (by moving some operations off the chain) in order to gain others. For instance, it is generally accepted that state transitions on-chain are expensive and impractical but two parties could agree to work off-chain to compute these state transitions while maintaining hashes of the state to keep each other honest.
This means that if one party decides to lie then the full weight of the blockchain will be needed to resolve the dispute but if both parties agree maybe the entire exchange could be just a few transactions.

As far as the practicality of blockchain and Ethereum I’m not sold that the technology is quite there yet.
In my opinion, it would seem that a solution that admits trusted parties is necessary while simultaneously trying to balance the scales between trusted parties and the greater decentralized network would be a successful approach. However, as previously stated, I am not a blockchain researcher and it is possible that there is still a satisfactory solution that is completely decentralized.

The state of Ethereum withstanding there are some cool projects and technologies that I also learned about at Devcon4. As one might expect from cryptography, mathematical results that were cast as having essentially no practical applications turned out to have practical applications.
In this case, that application is zkSNARKs and zkSTARKs. The acronym zkSNARK stands for zero-knowledge succinct non-interactive argument of knowledge. These mechanisms for automated proof verification are being applied to blockchain protocols like Zcash and potentially other poof of stake protocols. A very broad and quick overview of zkSNARKs is the “Where is Waldo” example.
Imagine that a child wants their parent to prove to them that they found Waldo. The parent, of course, doesn’t want to ruin the puzzle for the child by revealing where Waldo is but also desires to demonstrate that the puzzle is solvable. To solve the problem, the parent cuts out a hole from a large piece of cardboard the size of Waldo and places the puzzle behind it. Now, the child can only see Waldo and not the relative position of the puzzle behind the board. The child has verified the knowledge of the parent without the parent giving up the construction of that knowledge, so to speak. It’s a fascinating field and one wonders if there is anything useful for formal verification tools to learn from.

Another interesting project that also happens to be a grantee of the Ethereum Foundation is the Gitcoin project. Gitcoin is a Dapp (decentralized application built from smart contracts on the Ethereum blockchain) that allows users to post bounties on Github issues for other users to work on and then claim. In my opinion, Gitcoin is an admirable effort to energize the open source community by changing the story from volunteer passion work to actual work! Ideally, this project could be useful in helping those who simply can’t volunteer their time to find a foothold in the open source community to instead finance their contributions.

Finally, the Solidity team at Ethereum showcased the beginnings of their SMT integration. It wasn’t explicitly stated in the talk what SMT solver was being used, but based on some file names shown in the source code during the demo I can confidently say they’re exploring Z3 and CVC4. From my understanding, the way smart contracts are modeled is in functional units, so pre and post conditions of functions aren’t usable from the perspective of the SMT Solver in a separate function.It seemed to me like a good start. All the same, it was encouraging to see a team greasing the gears of automated formal verification in a programming language.

And that’s all! Devcon4 was a lot of fun and there was a lot to discover. The video recordings of talks are suppose to go up around two to four weeks after the final day of Devcon4.I recommend giving the talks a glance and watching anything you find interesting, there was a lot going on that I missed!

[1] http://hackingdistributed.com/2018/07/02/on-chain-vote-buying/

Advertisements

The following is a report from CS doctoral student Chris Jenkins, working with me here at U. Iowa, on his attendance at IFL ’18.

 

IFL 2018 Highlights

A couple of weeks ago I had the pleasure of attending IFL 2018, the 30th
Symposium on the Implementation and Application of Functional Programming
Languages
where I would be presenting the type inference system Aaron and I
developed for Cedille. I found the talks given over the course of the
symposium to be for the most part quite interesting, and even more so the
other attendees and dinner-time discussion, and so thought I might share of
the highlights with QA9’s readership.

First I would like to mention that the venue this year was quite lovely: the
UMass Lowell Inn and Conference Center. Lowell is a quiet little town 30m
outside of Boston where the streets curve through hills and pass under the
over-hanging branches of tall trees. The inn itself was quite nice, situated
as it was just south of a canal that fed into the Concord river. It was very
lovely!

9/5: Haskell GADT Tutorial

The first day was a rather friendly an informal tutorial on the advanced
usage of GADTs in Haskell, taught by José and David from Galois. The first
part of the session laid the foundation for developing a balanced two-three
tree whose depth was encoded at the type level, and how to go about writing
an insert function for such a type (after all, the depth of the resulting
tree might change!). Being more familiar with Agda than Haskell, I was more
curious about (and in some cases, amused by) the bag of tricks Haskell
requires to simulate programming with dependent types (here, unary numbers to
represent the tree depth). There was also some healthy skepticism in the
audience about whether the invariant we were trying to preserve (that the
depth remains the same, or grows by one, after an insert) was worth the extra
complexity required. The topic continued to be discussed during lunch at my
table – which is perhaps one of the greatest pluses for attending such
conferences in the first place! The latter half of the tutorial ramped up to
the more involved example of developing a verified type-checker for a toy
language of booleans and integers. Both repositories used in the tutorial can
be found here and here, for anyone interested.

9/6: First Day of Talks

The keynote for the first day was given by Adam Chlipala. In his talk, he
laid out what (to me, at least) seemed like a radical call to re-evaluate the
role of the “standard computational model” of functional programming
languages. The main idea was that most programmers are working in a domain
where the products being produced are variations on a theme, rather than
wholly new works, and specifically variations within a well-defined domain.
We look to FP as a way to provide certain correctness guarantees, but the
general-purpose run-time efficiency leaves something to be desired. Using SQL
as an example, Adam then proposed that not only would domain programmers
would happier with domain-specific languages, but compiler writers would be,
too! If the compiler could be provided (proven to be sound) rewrite rules
that hold for the domain, this could allow us to more easily (and safely)
explore different approaches to program optimization, and in the process
leave the “standard cost model” of functional programming behind. Quite the
talk to mull over!

In addition to the keynote, I enjoyed mostly all talks given. To single just
one out of the many that were given, the talk “Continuation Passing Style and
Primitive Recursive Functions” by Ian Mackie came from quite an interesting
observation. This appears to be one of those cases where one reads something
in the textbook and ask “But wait, why is that the case?” – and maybe a
decade or so later, you start to have an answer! To start, we know that any
program you want to write can be given in continuation-passing style, for
simple programs like multiplication (through repeated addition), the CPS
style can be further simplified into an accumulator style. The unanswered
question was “which CPS programs can be ‘optimized’ into an accumulator
style.” And in this talk, Ian gave the sound (though not necessarily
complete) answer that all primitive recursive functions can be written this
way, taking a detour into linear type theory along the way. Very interesting!

9/7: Second Day of Talks

The keynote of the second day was given by Arjun Guha, and actually I noticed
some broad similarity with Adam’s talk. Arjun presented work for verifying
different network layers, starting with the network policy layer with a
NetKAT, a high level (and principled) language for describing the policies
for accepting, forwarding, and filtering packets. He also talked about PANE
(short for PArticipitory NEtworks), a paradigm for the configuration of
Software Defined Networks (SDNs) that is able to handle live changes to
network policies and dynamic resource usage. More still was work on verifying
Puppet configurations (with Puppet being a language for declarative
specifications of a system’s configuration) have such desirable properties
as: determinacy (the configuration would always be executed in the same
way); and idempotency (a second execution of a configuraiton produces no
change on the system). There was much more, of course, but my big take-away
from this and from Adam’s talk was that there is a great opportunity for
formal methods to really shine in restricted domains.

If I must arbitrarily pick one of the many good talks given today, the one
closest to my own interest would have to be “Delta Debugging Type Errors with
a Blackbox Compiler” by Joanna Sharrad et al. The premise is intriguing –
how much can we improve type errors by treating the compiler as a black-box?
Using Haskell and GHC, they showed an interesting approach of bisecting
programs with type errors to find the smallest type-correct program, and the
smallest change on top of this that produces a type error, using this more
minimal example to help inform the programmer. Now, I do not thing that
language agnostic tools will ever beat gnostic ones as far as providing
useful feedback – but blackbox techniques open up the possibility of
experimenting with different error reporting across many different languages,
which as someone interested in improving type error messages (and the
usability of languages with advanced type features, more generally) certainly
caught my interest!

I have been interested, for many years, in what is generally called computational classical type theory (CCTT).  The idea is to take some proof system for classical logic, and turn it into a programming language via the Curry-Howard isomorphism.  Cut elimination or normalization for the proofs turns into reduction for the corresponding program terms.  There is nothing at all objectionable about this, and indeed it is very interesting to see term notations for proofs of classical theorems like ((A \to B) \to A) \to A (Peirce’s Law) or A \vee \neg A.  It was the brilliant insight of Griffin (my that POPL ’90 was a good one, as Lamping’s paper on optimal beta-reduction was that year, too) that proofs of such classical theorems essentially involve control operators like call-cc.  This is all super cool and very interesting.

And I accept what I understand to have been David Hilbert’s position that non-constructive reasoning is an essential tool for mathematics, and that rigid constructivism (i.e., insisting on constructive proofs for every theorem) is thus disastrous for advancement of mathematics.  In Computer Science at least, I have sometimes in the past thought that the ability to do things like case-split on whether a term in some unrestricted programming language terminates or not could be very helpful if not critical for verification of general programs.

Since Curry-Howard is great and applies very nicely to classical logic, and since classical logic is useful if not essential for certain kinds of verification, CCTT should be fantastic in my book, right?

No — and of course I will tell you why.

The problem is that the Curry-Howard isomorphism a reasonable programmer expects to hold is broken in CCTT.  The problem can be seen clearly with disjunctions.  Under Curry-Howard, a disjunction A \vee B corresponds to a sum type A + B.  Given an element of such a sum, we can case split on whether that element is the injection of an element in A or else in B.  And in doing so, we gain some actionable information.  But this does not happen when we split on a use of the law of excluded middle A \vee \neg A (LEM).  We gain no information at all in the two branches of the split.  And indeed, the usual way CCTT proves LEM is to say (so to speak): it is \neg A which is true.  Then if the branch of the split for the right disjunct ever tries to make use of that information — wait, how can it do that?  The only thing you can do with the negative fact that \neg A is to apply it to a proof of A to obtain a contradiction.  And if you ever do that, the machinery of CCTT will take your proof of A, backtrack to the point where it originally told you \neg A is true, and then invoke the branch of the split for the left disjunct, with that proof of A.  Super clever!  (This is dramatized by a famous story about the devil told by Phil Wadler; see my old post about this.)  But also, note that it means you can never take action based on the result of such a case split.  Everything must be indefinitely revisable, due to the possible need to backtrack.  So you cannot split on an instance of LEM and print 1 in the first branch and 2 in the second.  Or rather, you can, but the meaning is not at all what you expect.  “This Turing machine either halts or it doesn’t.”  We case split on this, and could easily think that we are gaining some information by doing so.  But we are not.  Your code will just always print 2.  This is not what you reasonably expect under the Curry-Howard interpretation of disjunctions.  And thus using CCTT for programming is not a good idea.

It would be fine to use classical reasoning for reasoning about programs.  For the justification of some property of a program might require (or be easier with) some non-constructive case split.  But the program itself should not do such things, or else the abstraction Curry-Howard seems to offer us is violated.

Is this an argument against sum types in the presence of control operators?  (Genuine question)

 

 

For loyal QA9 readers, advance announcement that our release of Cedille 1.0.0 (promised some time ago!) is going to be made Friday.  You can get a sneak peak at the web site here.  The links on that page to the github repo won’t work yet as the repo is private.  But this will change Friday.  We will have a Debian package for easy installation — and will be happy for pull requests for packaging for other systems!

I remember, from maybe grad school, being puzzled about “semantics”.  What does this word mean?  Having gained a lot more knowledge of this topic since then, I thought I’d share a few thoughts on it, especially in the context of type theory.

“Semantics” means meaning.  In this sense, many different approaches to the study of programming languages are described as giving some form of semantics to a language.  An interpreter gives you a semantics for a language.  It shows you what these funny sequences of keywords or symbols (or more modernly, these peculiar abstract syntax trees) mean by showing how the programs execute.  If one writes an interpreter as a set of inference rules, then this is usually called operational semantics.  Hoare Logic, which is a set of inference rules for verifying that programs started in states satisfying a given precondition will (if they terminate) end in a state satisfying a given postcondition, has traditionally been dubbed axiomatic semantics.  This term “axiomatic” is maybe not too informative, but the idea that you can describe the meaning of an imperative program by explaining how it changes the state indeed gives it a reasonable claim to be a semantics.  What do programs in the language mean?  A semantics tells you.

There was a lot of interest in earlier days on giving denotational semantics to programs.  The idea is to give the meaning of a program by stating what mathematical function the program denotes.  After all, programs are intended (are they not?) to represent some class of functions as understood in mathematics.  A hallmark of denotational semantics is that it is compositional: the meaning of a bigger expression is defined in terms of the meanings of its strict subexpressions.  Notice that this is not true of operational semantics generally: we define the meaning of (\lambda x.\, t)\ t' in terms of [t'/x]t, which is not a strict subexpression of t (indeed it can be a bigger term than t). There was a lot of excitement, it seems, in finding denotational models of languages like lambda calculus.  More recently, it seems more common, at least in Computer Science, to take lambda calculus for granted and not be concerned with mathematical denotations of lambda terms.

Logic is, as far as I know, the earliest field concerned with giving mathematical semantics for formal languages.  There, denotational semantics of formulas is the basis of model theory.  Proof theory can also be viewed as giving a semantics of formulas, and indeed in nice situations these two semantics agree — though even for theories like first-order arithmetic, results like Goedel’s incompleteness theorem imply that no such agreement is possible: the proof-theoretic semantics (showing what formulas mean by showing how to prove them or use them in other proofs) must be weaker, in the sense of proving fewer theorems, than the denotational semantics.  But maybe this is a digression…

In type theory, there is a great tradition of giving denotational semantics for types.  In full generality, if we have a term t of type T (in some typing context G!), we would like to explain what this relation (G \vdash t : T) means.  Historically, it was discovered that one could use a denotational semantics for types as a proof method to show deep properties of the language, like normalization or logical consistency.  I first learned about this in Girard’s Proofs and Types, and still recommend this as a good introduction.  The historical root of this is Kleene’s realizability semantics for first-order intuitionistic arithmetic.  But one does not need to be driven by the desire to prove such metatheorems, in order to want to have a denotational semantics for types.  Here are my amazing new types!  Wouldn’t you like to know what they mean?  I can show you some typing rules, and depending on how I set them up — for example, if you give introduction and elimination rules for the types that are related in certain ways — these could to a greater or lesser extent show you what the types mean.  But a compositional semantics that says, “my funny type construct X A B means …” can be more direct, and provide guidance for crafting typing rules.  One can prove that a set of typing rules is sound with respect to the semantics, for example.

The form of such semantics I have found most useful is a realizability semantics, that tells you what a type means by specifying the set of all terms whose operational behavior is allowed by the type.  For example, in some language, the meaning of a type like “Int -> Int” could be defined to be the set of all programs which, given an Int input, either diverge or produce an Int output.  Or maybe in some other language, it is the set of all terms which, given an Int input, are guaranteed to terminate producing an Int output.  Notice that these example semantics do not say anything about the internal form of the program.  It could fail to be well-typed according to some set of typing rules.  It could do very crazy and upsetting things if not given an Int input.  The only thing the type specifies is the behavior of the term when given an Int input.  So the type describes behavior of terms, through the simple device of giving a set of terms as the meaning of a type (namely, the set of all terms whose behavior is allowed by the type).

For Cedille, I have defined such a semantics, and used it to prove logical consistency of the system.