Our great sponsors
-
juvix
Discontinued Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
https://gitlab.com/morley-framework/morley (~similar to https://github.com/input-output-hk/plutus on cardano)
and in the future: https://juvix.org/ (This stuff is just ridiculously advanced)
https://gitlab.com/morley-framework/morley (~similar to https://github.com/input-output-hk/plutus on cardano)
The link to the Coq formalization of Michelson, to formally verify smart-contracts: https://gitlab.com/nomadic-labs/mi-cho-coq
That being said, being written in a functional style helps a lot and OCaml helped to enforce a functional style. We made a translation to Coq of the protocol in https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml using https://clarus.github.io/coq-of-ocaml/ , a tool which we mostly developed for this project. It should now be possible to prove many properties about the protocol. I believe we could have done the same thing with any programming language, as long as the source code is written in a functional style.