SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon

Re:SafeDollar ‘stablecoin’ drops to $0 following DeFi exploi... by solomonb on Tuesday June 29, 2021 @03:59AM (#27673115)

Ok I did a really shallow search of the smart contract space and it looks like the trend is towards creating simple languages that are easy to reason about and formalize their semantics. Simplicity seems to be the best example of this.

With such a language you can write proofs about the behavior of the runtime using some proof checker and then programs in it should be simple enough to reason about in a rigorous way.

What I have not seen and what I am curious about is a smart contract language more in the spirit of Idris. That is to say a more complex language design with full dependent types, which would be a lot more difficult to formalize, but would allow you to do really nice things like treat proofs as first class citizens in your actual smart contracts.

[ Parent | on HN ]

Re:SafeDollar ‘stablecoin’ drops to $0 following DeFi exploi... by wyager on Tuesday June 29, 2021 @08:55AM (#27675125)

I think in most cases you wouldn’t want something like idris as a smart contract language on any kind of cryptographic system (blockchain, ZKP system, whatever) because idris programs are expensive to typecheck and evaluate. It would be reasonable to construct a DSL or something in idris that compiles a compact, easily computable language though.

The idea about having proofs as values in smart contracts is interesting though. I could see a few neat applications of that.

[ Parent | on HN ]

Re:SafeDollar ‘stablecoin’ drops to $0 following DeFi exploi... by solomonb on Tuesday June 29, 2021 @02:42PM (#27680008)

Yeah I agree that Idris itself would be much too large, however you could write a much smaller Lambda Pi that could still enable a lot of nice features.

[ Parent | on HN ]