Given that to meet constant-time requirements, the language will need to guarantee more or less 1-for-1 (or more generally, M-for-N) translation to assembler, I

Given that to meet constant-time requirements, the language will need to guarantee more or less 1-for-1 (or more generally, M-for-N) translation to assembler, I don't think you're going to improve on the verification or type checking situation by changing the syntax to something else.