Idris language using Qtum x86



  • Hi there,

    So on Saturday (25th November) Patrick came to Hong Kong and talked about QTUM at "Genesis Block", thanks for coming. So what I was thinking was, as I am a programmer it would be nice if a computer language Idris could work in QTUM's contracts as the contract language due to the fact that you can verify that functions terminate and verify their correctness.

    Some effort had been done to bring Idris to Ethereum in the past with this https://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf
    Their code https://github.com/vindaloo-thesis/idris-se

    However it is "Idris to Serpent" and not efficient in implementation so not really practically useful due to inefficiency. What would be good is if the x86 VM your doing can allow for Idris to run then we can have nice formally checked functions running on QTUM, both the Idris community and smart contract people would find that useful if it is efficient and practical.

    Some could say Idris is not familiar to ordinary programmers, its more in the style of Haskell, well the academic people who are familiar with Haskell would then find it easy to come to QTUM contracts using Haskell style programming (Idris).

    Then your doing some work in the Scala language, what is that?

    Why do x86 VM? Why not the JVM? Why not another VM such as dotnet? Why not a Javascript VM? (would a Javascript VM be too slow, I don't know enough).

    Thanks, Philip


Log in to reply
 

Looks like your connection to QTUM was lost, please wait while we try to reconnect.