Just to add, things like type checking are the comparatively easy part. The world itself and many of our constructs for thinking about it are not well defined.

Just to add, things like type checking are the comparatively easy part. The world itself and many of our constructs for thinking about it are not well defined. The trouble in reconciling these things are why things like appeals courts exist. Smart contracts built on this ill defined world will always have bugs. The world isn’t going to become significantly more well defined for smart contracts, either. If that were possible, we wouldn’t have those aforementioned higher courts.