Interesting topic! I think this relates to the EVM's Solidity smart contracts running out of gas, and Liquid Simplicity solving that problem with computation safety assurances. They use Coq as well, that's why I think there is a connection.