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)

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.