Provable vs. Composable Computation or why Cairo will supersede Solidity

Summary. In this post, I will argue that Cairo can effect the coming wave of provable computation in the same way that Solidity has enabled composable computation. Cairo is the native programming language of StarkNet, a Layer 2 network designed to scale Ethereum.

—

It's regrettable when we see smart contracts merely as an extension of finance (DeFi) or a generalization of the web (web3). Smart contract networks are really platforms for composable computation.

Ethereum embeds certain standards that allow its computer programs to interoperate:

• Transparent byte code (no hidden web APIs)
• Standardized API structure (called the ABI)
• Guaranteed uptime (each app is hosted on multiple machines, per-app Denial of Service is uneconomical)
• Built-in payment infrastructure (no reliance on 3rd parties like Stripe)
• Full deployment and transaction lineage
• Friction-less contracting between different application layers (governance, ownership, etc.).

These constraints can impair developer productivity (see critiques of web3) but has also incentivize composition and re-use of stateful applications at an unprecedented scale.

Solidity was the first mainstream language for composable computation

Solidity was created as a simple language that is compatible with the above standards. It provided:

• Basic state machine functionality (state, access, updates, etc.)
• No access to non-composable primitives (e.g., external data feeds)
• Interfaces for contract-to-contract interaction (means of composition)
• Built-in gas metering for transaction fees
• Performant access to the underlying virtual machine (assembly).

While existing programming languages can be adapted to service composable computation, they need a combination of extension (adding interfaces for composition) and restriction (removing all forms of non-determinism and external access) that is difficult to incorporate. Moreover, the compilers of these languages were defined to optimize a completely different performance metric (execution footprint) than is required to optimize Solidity code (gas costs).

Introducing Provable Computation

StarkNet's scalability tool, ZK Roll-ups, enable a new paradigm called Provable Computation. In this paradigm, we retain all the benefits of composable computation but also allow programs to prove they have been executed without having to be re-run.

This simple idea allows us to move from a network (Ethereum) where validating a transaction requires re-running it to a better network (StarkNet) where transactions are validated by validating the proof that they have been executed with a certain outcome, a much more economical operation.

Because this paradigm is so different, it also requires a different computing model, effectively turning programs into number theoretical equations rather than executing them on a machine.

What programming language could we use possibly use for this?

Solidity vs. Cairo

It's natural to consider Solidity. For one, it already supports composition (calling other smart contracts) and is widely adopted. Two, there are a range of applications that are deployed on Solidity that can be easily migrated to other Layer 2 solutions (including zkSync which supports Provable Computation). Three, Solidity has a well-maintained multi-layer compiler that can be adapted to serve different use cases.

But Solidity is not native to provable computation. Any compiler that takes idiomatic Solidity code and translates it into proofs will struggle with the following issues among others:

• Reliance on inefficient data structures like uint256 and operations on them
• Mutability at the language level
• Lack of efficient built-ins
• No low-level access.

Technical detail. In practice, there are 2 different technologies for proving general programs (SNARKs and STARKs). Instruction sets favored by SNARKs are better suited as a compilation target for languages like Solidity. STARKs offer more scalability while having a less natural instruction-set. So when we say “Solidity is not an efficient language for provable computation, we really mean two things: 1) Solidity can be efficiently encoded to SNARKs, but they are not as scalable as STARKs 2) Solidity is not the optimal language to compile to STARKs since constructs that are common in Solidity are “costly” for STARKs. [1]

Cairo has solutions for all the above:

• A low-level field integer data type called felt is available (alongside a uint256 type)
• The Cairo language is idiomatically write-once (like a functional programming language)
• A growing list of built-in non-deterministic hints is being developed for common computations
• Cairo provides full low level access to underlying primitives. [1]

Yes, programming in Cairo is also more challenging and ecosystem tools are still maturing. But the whole point of scaling Ethereum is to transcend existing limitations and build better composable applications. If so, why stop at Solidity?

Surf the paradigm with us

Interested in the potential of provable computation on StarkNet whether as a developer, investor or user? Join our Discord.

—

[1] Cairo Whitepaper, https://www.cairo-lang.org/cairo-whitepaper/