Idris language using Qtum x86
philip368320 last edited by
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?