Are there even any dependently typed smart contract languages that would allow you to encode and carry proofs in your contracts?

Without that I think the best you could do is model your program in some other formal verification system and then convince yourself that your model matches the actual contract.

The Simplicity language is good. I’m sure there are other designs.

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.

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.

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.

Ever heard of Cardano?