Most smart contracts on Ethereum, or other blockchains are only immutable in their marketing material, but not in practice. Either they use an obvious PIMPL/Pro

Most smart contracts on Ethereum, or other blockchains are only immutable in their marketing material, but not in practice. Either they use an obvious PIMPL/Proxy contract (OpenZeppelin, a popular smart contract library suite has proxy contract that many others use: https://docs.openzeppelin.com/upgrades-plugins/1.x/proxies https://docs.openzeppelin.com/upgrades-plugins/1.x/proxies), or they have other subtler hooks that can be used to change what ABI/function calls to the smart contract does. These hooks are only usable by privileged actors (surprise surprise). Smart contracts being immutable is a joke, almost. And more importantly, even if they were immutable, proving that formally for a Turing complete language is impossible. Bitcoin smartly avoided this by making its smart contracts dumber.