Cardano [ADA] community and the CEO of Runtime Verification discuss the Cardano Protocol

Recently, the Cardano Foundation posted a Webcast on Twitter wherein Jon Moss, a member of the foundation’s Marketing and Community team spoke to Grigore Roșu, the president and CEO of Runtime Verification. The interview was focused on answering questions from the Cardano community in relation to the research and development of the Cardano Protocol that Runtime Verification is overseeing.

IOHK in collaboration with Runtime Verification is set to develop a new technology built on formal semantics for the Cardano Foundation which includes a new virtual machine. Through the partnership, IOHK and Cardano have launched two Cardano Smart Contract testnets, the KEVM testnet and the IELE testnet.

The KEVM testnet is a correct by construction version of the Ethereum Virtual Machine that has been specified in the K framework [formulated by Runtime Verification]. The IELE testnet is a register-based virtual machine. A viewer from the Cardano Community asked:

“In your opinion, what would be a better solution for deployed code? Do you want to allow the use of any imports and K resolves them transitively? Or would you rather only allow “native” built-in syntactic structures for a language, without allowing any imports, so developers would manually add any required utilities with each contract?”

Grigore Roșu in his reply stated that both approaches are possible. According to Rosu, the plan is to take any programming language for regions of formal semantics in the K Framework and generate a compiler from that language to the IELE testnet. The team would then run IELE natively on Cardano. Rosu said:

“The question now is how to deal with libraries. One approach is to have built-in libraries in IELE itself wherein all the languages will be integrated into the IELE testnet. The other option would be to have implementations of various libraries in IELE or translations from those libraries.”

According to Rosu, what will finally happen is a mixture of the above two mentioned scenarios. Experimentation is key at the moment, and user input will be extremely useful as well, he added. Rosu Said:

“What we have in mind right now is to have a basic set of functionality that will be provided IELE already. And this is in terms of how to check balances of different accounts for example or how to make a transfer from account A to account B.”

IELE has a built-in API which is why it functions at the core level. Therefore, a whole library can be integrated into an account. All the developer has to do is, make a ‘call action’ to the account and its core functions. As these arguments are in IELE, the developers can make use of them in higher-level languages.

Rosu further stated that when a developer wants to define the semantics of a specific language, there will be a way to hook commands or statements in that language. Developers can also hook fashion names in a particular language to the library names that have already been provided by the IELE library. They are going to have a library implemented in IELE either generated from higher level languages or even directly by hand in IELE. Rosu concluded by saying:

There will also be some built-in functionality in IELE that is already being used for some basic operations. And then there will be a way in which the language semantics that are defined in K Framework can hook operation symbols in a specified language to this library function.”