Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Ben Siraphob
    @siraben
    @sshine Agreed with the lack of product and sum types in smart contract languages, especially since the benefit of representing data types like that allows generic programming to really work.
    Ben Siraphob
    @siraben
    Glad to see that work has been done on verifying increasingly complicated contracts, too.
    Simon Shine
    @sshine
    Oh god I could use some proper high-level math libraries in Solidity.
    I'm collecting a wish list for a better general-purpose language, @siraben. ;-)
    Ben Siraphob
    @siraben
    @sshine Would be interesting. Do you know if a total functional language has been written for smart contracts?
    Codata also seems like an elegant solution to needing infinite processes in a total language.
    Simon Shine
    @sshine

    @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. :)

    Ben Siraphob
    @siraben
    I also highly recommend the Total Functional Programming by John Hughes which talks about codata as well.
    Total as in every expression has a well-defined meaning (i.e. the absence of bottom values). Exceptions can still take place but in a safe manner, for instance, through a monad or effect system.
    Simon Shine
    @sshine

    @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 view and 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.

    Ben Siraphob
    @siraben
    @sshine Oops got the author wrong, it's David Turner's Total Functional Programming.
    @sshine So like a way to indicate effects à la MTL or Extensible Effects?
    Simon Shine
    @sshine
    Yes!
    Like, "this call transfers money to party <A>!"
    Ben Siraphob
    @siraben
    Looks like some values would go to the type level too like addresses and wei.
    Simon Shine
    @sshine
    Yeah, I think you could get away with some very natural use-cases for dependent types.
    Simon Shine
    @sshine

    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.

    Ben Siraphob
    @siraben
    @sshine It's about it I think, there's not much activity in this space.
    There was a mature (to my knowledge) Scheme to EVM compiler I saw sometime a year or two ago, Pyramid Scheme
    The Plutus language has a strong research background too
    Simon Shine
    @sshine
    I might provide a category of "languages that looked promising but where the last commit is in 2018" as that seems to cover at least a few languages. ;-)
    Ben Siraphob
    @siraben
    Heh, indeed.
    Ben Scherrey
    @scherrey
    @sshine would definitely love to see that talk.
    Simon Shine
    @sshine
    @scherrey: I give it some time in week 34, I think. I might post the slides before for feedback.
    Ben Scherrey
    @scherrey
    cool
    Ben Siraphob
    @siraben
    @sshine Where's the place to discuss Lira?
    Simon Shine
    @sshine
    @siraben: Open an issue on GitHub or send me an email. :)
    Ben Siraphob
    @siraben
    @sshine Oh great, there's also papers in the README as well.
    Ben Siraphob
    @siraben
    @sshine How does the implementation of Ethereum implement observables? Through some oracle?
    Ben Siraphob
    @siraben
    Lira on Ethereum*
    Simon Shine
    @sshine

    @siraben: Yes, the EVM back-end assumes a .get(bytes32) -> int256 interface:

    https://github.com/sshine/lira/blob/master/src/Lira/Backends/Evm/EvmCompiler.hs#L699

    One goal is to get Chainlink support instead.

    Ben Siraphob
    @siraben
    @sshine Ah I see. One thing that surprised me was that calculating contract horizons in that paper could be undecidable if exponentiation was added.
    Simon Shine
    @sshine
    @siraben: Can you elaborate?
    Simon Shine
    @sshine
    @siraben: As in, what is "that paper"? :)
    Oops not that one
    " implement this rule we have to check whether the derived transfer function for the contract c is equal to T0, the empty transfer function. This is undecidable if we use the full function space Trans of transfer functions."
    Ben Siraphob
    @siraben
    @sshine lira has been moved under a new owner? https://github.com/etoroxlabs/lira
    Simon Shine
    @sshine

    @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.

    @siraben: His repo is still private (not sure why) and my repo that I posted on IRC earlier was only opened for debugging Data.Fix. :-P
    @siraben: There is still not much to see, I guess.
    @siraben: But my evm-opcodes library is soon ready for release :) https://github.com/sshine/evm-opcodes/
    Ben Siraphob
    @siraben
    @sshine Exciting. Have you heard of the https://hackage.haskell.org/package/hevm library?
    Looks like the have a EVM.Opmodule as well but it's not the main purpose, glad to see you're making a library that will focus on opcodes.
    Simon Shine
    @sshine
    @siraben: Yep, I forked Hevm and replaced their EVM.Op, but only later realized that their interpreter is written in a very low-level way that doesn't actually use the EVM.Op type. This one is purely used for pretty-printing opcodes. I'd probably end up making the interpreter initially slower if I turned it to use the abstract type rather than hex bytes, so I've post-poned adding my library as dependency, since then Hevm seems to prefer bytecode as serialization format, which is fine for now.
    Simon Shine
    @sshine

    @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