Hacker News new | ask | show | jobs
by Paradigma11 1859 days ago
There are some interesting projects on Tezos in this regard:

https://archetype-lang.org/ is a non-turing complete dsl that you can run http://why3.lri.fr/ proofs on.

Another way is to run proofs on the michelson that was generated by a higher level language (https://ligolang.org/, https://hackage.haskell.org/package/morley ...) with: https://gitlab.com/nomadic-labs/mi-cho-coq

The most interesting project (still alpha i think) to me is: https://juvix.org/ a rather elegant dependently typed language.

1 comments

Thanks for those. I really like the work that Tezos has been doing and the more I see from them the more impressed I am.

By the way what's your thought on Plutus (https://developers.cardano.org/en/programming-languages/plut...)?

It's technically its own language however it is basically a Haskell DSL/library that lifts code into a smart contract domain. It seems to retain the full expressivity and safety of Haskell (and the Haskell tooling). Additionally it allows you to share the same code base for on and off network code (as the smart contract code is largely just code lifted into a smart contract domain. This provides pretty much seamless interaction between the two domains. The documentation is a bit sparse at the moment which is its biggest weakness however that's rapidly being improved with the approach of Alonzo at the end of July/start of August.

I'm honestly so glad we as a space are finally starting to move away from Solidity and all of its footguns.