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.
-
Show this thread
-
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.
4 replies 3 retweets 53 likesShow this thread -
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.
8 replies 1 retweet 41 likesShow this thread -
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.
15 replies 2 retweets 66 likesShow this thread -
Replying to @TimSweeneyEpic
This is the thing that people need to understand. People have come to conflate “high level” with “in a separate universe from concerns with the CPU”... but the right idea is to connect from the high level all the way to the lowest level, and you adjust level as needed.
3 replies 4 retweets 50 likes -
Replying to @Jonathan_Blow @TimSweeneyEpic
Rust is the closest thing we have to that today. For example, signed wrapping arithmetic operations exist in the CPU but were effectively removed from C/C++. But they exist in Rust (if a bit verbosely).
1 reply 0 retweets 8 likes -
And ℤ/2³²ℤ is a perfectly fine mathematical object, it's just that most of the time you want to imagine you're actually in ℤ but with the additional invariant that you're not overflowing. Rust gives you the choice.
1 reply 0 retweets 3 likes
The fact that right shift of a negative number is UB is not being close to the machine, it's a delusional fantasy of being able to abstract over a class of machines that includes non twos complement (fortunately to be fixed in C/C++2x).
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.