iele-semantics VS lion

There hasn't been any development in that projects github in almost two years. Was that a prototype? Has that functionality been shelved? What am I missing?

The only parts that have yet to emerge are RINA, IELE, Scaling, and the Governance parts of the project. From what I can tell, scaling is 10-25% complete, IELE/K framework is at least 50% done, RINA might be impossible with internet's hardware, and Governance is being iterated upon with each catalyst proposal..let's say 45% finished.

It's still being actively developed and you can follow the development of IELE here: https://github.com/runtimeverification/iele-semantics/ . Since Cardano is a UTXO-based blockchain, it would need to run in an accounting-style sidechain (which is still an active area of research for POS blockchains)

Wait for the "ocean" of languages that will be introduced to Cardano via iele-semantics - meaning one day I will be able to code smart contracts in Python.

I've been starting to dabble with digital logic design via Clash (https://clash-lang.org/), and there is a very cool-looking RISC-V SoC project done in that tool that looks fairly serious: https://github.com/standardsemiconductor/lion.

That’s fascinating about the M1. In retrospect it seems like kind of a no-brainer but I doubt I would have thought of it.

SPARC had different memory models at different ISA revs IIRC: it’s been like 20 years since I was dealing with SPARC so I might be misremembering the details. Alpha would have been a better example.

RISC-V is really interesting. I’ve been slowly working through this: https://github.com/standardsemiconductor/lion, highly recommend!

Interesting. Actually, you may be just the person to answer my question: Is it possible/plausible to run a Cardano node on Lion OS on a RISC-V machine? IMO, it would be great for the community if we could run all Cardano stake pools on end to end formally verified machines using open source core and hardware.

Lion: A formally verified, 5-stage pipeline RISC-V core\ (30 comments)

In addition, you can actually set the riscv-formal suite to verify correctness by k-induction: https://github.com/SymbioticEDA/riscv-formal/pull/28 https://symbiyosys.readthedocs.io/en/latest/quickstart.html#beyond-bounded-model-checks although I concur that by looking at https://github.com/standardsemiconductor/lion/blob/main/lion-formal/app/Main.hs the lion core is only verified with BMC.