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.
The underlying DAG idea has potential. You could have two half-transactions happening on separate subtrees, where A is buying X from B and B is paying Y to A. So A broadcasts "A will buy X from B when B pays Y to A", and B broadcasts "B will pay Y to A when A buys X from B". When the matching half-transactions acquire a common child, the transaction commits. It's a true "meeting of the minds".
You can for example trade user-defined (possible private) assets (tokens) in that way - "Ill send you my bytes for your blackbytes, I send bytes to this address and me can sweep them back after 4 hours, or you can sweep them if payment of X amount of blackbytes is made to my address". It has oracles as well.
I only wish people had to do that. Shit like this are why professional and civil engineers roll their eyes at the mention of software "engineering". There are best practices and available tools but people employ them far less often than they probably should. In the space, take a look at Kadena's Pact smart contract language. It's not perfect by any means (lisp-religious syntax and its tight integration with Kadena internal constructions, for example) but it is at the least, working on formal verification support.
> This would be a stupid decision in any language
What kind of brain-dead apes designed this language? This would be a stupid decision in any language, never mind one specifically intended for high-value transactions.