> writing safety properties in a higher-level language, >This is true, and also insurmountable - the chain of correctness has to start somewhere. Exactly! W

> writing safety properties in a higher-level language, >This is true, and also insurmountable - the chain of correctness has to start somewhere. Exactly! We can shift the "correctness" test to correspond with the spec of the hypothetical higher language. But, we haven't actually solved for universal correctness as it corresponds with how humans would ultimately decide what's correct. In other words, the following function can be (trivially) formally verified: int increment_by_one(int x) { return x+1;} If int is signed 32-bits, one could brute force the tests for all 4,294,967,295 possible inputs. If x happens to be 2,147,483,647 and depending on the higher-level spec, one could define "correct" to abort with an error, or simply wrap around to a negative number. However, the standard of "correctness" for Ethereum is much higher than that. Let's say there's an unwanted event called Humans Will Decide To Fork Ethereum Because Of Unforseen Solidity Behavior which we'll abbreviate as HWDTFEBOUSB. I contend the following static checker that correctly returns TRUE or FALSE is impossible to write: bool HWDTFEBOUSB(string Solidity_code) In the context where you mentioned "insurmountable", I believe we are using the same frame of reference and are in agreement. Is my insistence on universal correctness an unfair standard? I don't think so because Ethereum creators wanted the programming code in "smart contracts" to be the ultimate and final arbiter. No follies of human judgement or politics to "pollute" the transactions. If that's the goal, just using a higher level language as a specification language for formal verification engines is not enough.