I also like this one, from the same article:
In other words, I do not want the compiler to just insert code to uphold the bare minimum guarantees, I want the compiler to check my work for me and assist me in developing an algorithm I can confidently assert is right.
(For example, I don't want the compiler to just make all the operations unordered and call data races solved, as in java, but to have it help me not write data races in the first place.)