@siraben: by total do you mean exception-free? many contracts may fail the preconditions of a call.
I'd like to create an overview of interesting contract languages today. I'm not currently aware of that many.
Also, I don't know anything about codata, but I've found the "Codata in Action" article and added it to my reading list. :)
@siraben: Is that the "Why Functional Programming Matters" article?
It is hard not to have total semantics when a contract isn't really allowed to fail beyond ending its execution. So you can count the number of ways that an EVM contract can end (
STOP, running out of gas,
JUMP outside allowed memory, or some similar break of invariants) and encode them as part of your return type, and you will trivially have avoided bottoms. So for a high-level language without access to inlining EVM opcodes, I doubt any of these apply.
I wonder if there's any point in encoding external contract calls (e.g. token transfer calls) as part of the type system, kind of like F*'s
Tot or Haskell has-style type classes. So while a function might have a simple signature wrt. its input and output values, its external contract calls could be considered side-effects.
To some extent you get a kind of safety in Solidity via the
pure modifiers. But you can't specify that "This function will only (and perhaps even exactly) make this-and-that call". You could even extend the
view modifier to grant particular memory access (rather than the full state).
I think these might be useful type-system features in reasoning about what a contract can do.
I'm preparing a talk on the development of blockchain languages for a small hacker festival.
Could you guys help me namedrop the most popular (so non-deprecated) blockchain languages?
The motivation for my talk is to get and provide a better overview.
So far I've got: Etherem[Solidity, Vyper], Tezos[Liquidity], DAML (as a representative of another kind of blockchain language).
The list feels kind of empty, so I'm also covering Lira as a non-general-purpose language because I happen to develop on it. But if I weren't, I probably wouldn't know, since it's been a long time since something new was published.
@siraben: Yes, the EVM back-end assumes a
.get(bytes32) -> int256 interface:
One goal is to get Chainlink support instead.
@siraben: So, Lira is property of eToroX Labs. They prefer that the git history is squashed for some reason, and I don't, so etoroxlabs/lira has the latest version and sshine/lira has the latest version with git history. The language/compiler used to be called 'Dagger' by the original author, Thorkil. He recently pushed for some changes and named his compiler Dagger2. The changes to the syntax is minimal, but the runtime is supposedly a bit different.
I'm in Switzerland these days helping him improve on his version of the compiler. In that process I'm rewriting the base Contract types for better use.
EVM.Opmodule as well but it's not the main purpose, glad to see you're making a library that will focus on opcodes.
@siraben / everyone else: What is the closest to a formal spec of EVM?
Upon revising my opcode library, I realized that opcodes have been renamed and added since the yellow paper I looked at some years ago.
Some of these changes were not even in the most recently published yellow paper. So old versions of the yellow paper circulate.
How do I make sure that I get notified when my derivation of the closest there is to a spec deviates from my implementation?
Currently I have to hope that the Hevm guys at DappHub keep a closer eye than me. :-D