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 @Anka213
Rust is C++ minus powerful template abstraction features plus stronger safety guarantees through shifting proofs of liveness to the programmer. Kind of one step backward and one step forward, not any closer to ideal.
1 reply 0 retweets 3 likes -
Replying to @TimSweeneyEpic @Anka213
What do you mean by lack of template abstraction features? I would say with macros and typeclass-like traits you don't lose that much powrr? Unless we're talking variadic templates or something.
1 reply 0 retweets 1 like -
The compile-time evaluable subset of Rust is sub-Turing and doesn’t support expression evaluation. It’s more like Haskell type class constraints than metaprogramming.
4 replies 0 retweets 2 likes -
Replying to @TimSweeneyEpic
Sub-turing doesn’t necessarily mean much. If you need to evaluate something that is not known to terminate at compile-time you are doing something pretty strange. Agda and Idris are both sub-turing.
1 reply 0 retweets 0 likes
Though sub-Turing, they do allow compile time computation of values to contribute to dependent types. Without that, common families of types require reinventing compile-time versions of things like integers, as in C++ pre constexpr.
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.