There are two interesting extremes of platform independent programming language design. One maps to hardware operations without surprising overhead, and another maximizes code correctness and verifiability by obeying all expected mathematical and set theoretic properties.
The first one is the C++ language. Disregard the byzantine standard libraries, syntax, and overload resolution rules, and it’s just a typed macro assembler.
The second one doesn’t really exist though CoQ and AGDA go in that direction. They support proofs-as-programs but aren’t quite real programming languages and have weird properties like rational numbers not being a subtype of integers.
Generally, I think the high level language could be layered onto the low level one through expanded libraries and constraints on unsafe operations, making a nice interoperable stack from top to bottom, with a unified and much more regular syntax than the status quo.
