The idea is that their approach does far more to integrate formal validation into a day-to-day development flow than to go for full Coq. They are currently working with Cadena people for Smart contracts integration, but not with Tezos.
I remember a while back someone added the ZCash Sapling Circuit written in OCamL (I’m not sure of the current status.)
I have a feeling that within the next year or so we’ll have ZK-Snarks proposed for a vote. Not sure whether they’ll be used for private transactions, but I think I remember reading a medium article where Arthur proposes using Zero Knowledge Proofs to scale the protocol as opposed to Sharding.
I believe in substance, not hype.
Saying this is great technology is one thing, demonstrating that it works is all that matters. So let’s prove it!
Besides, while the token prices are low, we should take advantage of this opportunity to experiment like hell. Once this becomes a multi billion dollar chain, we can’t afford as many critical mistakes.