Just looking at this language, it makes me feel like we are going back in time in regards to readability and ease of use. I understand that security and provability of contracts is more important in these cases, but one can dream!
Michelson is a VM bytecode, not a programming language, although it happens to be readable enough to write simple contracts in it directly.
IIRC, the old Camllight VM was pretty similar (I might misremember, that was literally decades ago); an ML-like language to Michelson compiler is fairly straightforward to write and to prove sound.
I'm happy that they do things the sane way, i.e. focusing on sound foundations rather than on how Javascripty the syntax looks; but I'm afraid the communication isn't as clear as it could/should be. Blessing a compiler for some subset of ML, as a first high level language, would have cleared things up IMO.
