Bamboo compiler started producing EVM bytecode

It’s been nine months since I started working on the Bamboo compiler. There was a long dormant period, but this week the compiler started emitting some bytecode. Some of the compiled code even work as intended. So, have a look at the GitHub repo or join the Gitter room (especially if you write OCaml; the compiler is written in OCaml).

Bamboo is my answer for designing a reasonable programming language for Ethereum contracts. By reasonable I mean easy to reason about. Especially I chose to make it explicit what can be called when.

In all existing programming languages for Ethereum, any interface can be called at any time by default. Additional checks would prevent untimely calls to wrong interfaces, but the outermost structure does not show when to call what.

contract CrowdFund {
	function toBeCalledDuringFunding() {
		// perhaps check it's during funding
	}
	function toBeCalledAfterFailure() {
		// perhaps check it's after failure
	}
	function toBeCalledAfterSuccess() {
		// perhaps check it's after success
	}
	function notSureWhatThisDoes() {
		// This can mess with all other code.
	}
}

In Bamboo, the outermost structure shows the modes of operation.

contract Funding() {
	function toBeCalledDuringFunding() {
		// something something
		return true then Funding();
	}
	function endFunding() {
		if (something)
			return (true) then FundingSuccess();
		else
			return (false) then FundingFailure();
	}
}
contract FundingSuccess() {
	function toBeCalledAfterSuccess() {
		// something
	}
}
contract FundingFailure() {
	function toBeCalledAfterFailure() {
		// something
	}
} 

Now you see three contracts, but they are not deployed separately. One becomes another. See the line return (true) then FundingSuccess(). This makes the contract become a FundingSuccess() contract. Only after that, toBeCalledAfterSuccess() function is accessible.

This looks a bit like a state machine, and actually it is. The language forces the state-machine approach to programmers. Every time the control flow is lost, the programmer needs to say “then” and specify the left state. Even when the contract calls something, since that something might call back, a state needs to be specified.

You can specify the next state. So there is no need to assign values to state variables. There are no state variables, but only arguments to the contract constructors. When you want to store a number, you just put it as an argument of the next state.

contract box (uint bid)
{
   default
   {
      return (true) then box(value(msg));
   }
}

After a call into default the contract behaves as if it’s deployed with new box (value(msg)). So, every call constructs and deploys a contract in-place. You don’t have old clutters in your contract. It’s always fresh, somehow.

How does this connect to formal verification? I’m supposed to be working on proving Ethereum contracts correct. Some contributors and I are making changes in the reasoning framework. There I learned how to reason about Ethereum contracts. When I tried to specify an Ethereum contract in Isabelle, I ended up specifying several modes. If that’s the way to reason about contracts, maybe that’s the way to write contracts.

Currently I’m confident I can write an interpreter of Bamboo in Coq or Isabelle/HOL. I don’t want to expand the language much further until I write one so that I can prove properties of Bamboo programs. Ultimately I’d like to replace the compiler with a proven-correct one, but for that, a Bamboo interpreter needs to exist in a theorem prover.