3 ms·
They are all converging on these features because they have proven universally useful. But there is still a lot of work going on about other, new features. Some
by tomp 12y ago
They are all converging on these features because they have proven universally useful. But there is still a lot of work going on about other, new features. Some examples that interest me:
- effects and exceptions - should we use monads (Haskell), macros (Rust), handlers (Eff, algebraic effects), extensible rows (Koka)
- memory usage - how should we handle deallocation - using reference counting with infrequent GC (Python) or by being very careful (C++), using just GC and allocating freely (OCaml/Haskell, Java & Nim use "realtime" GC), using uniqueness semantics (Rust, ATS), using memory pools and great care (Objective C) - none of these approaches is perfect and optimal for all situations, and it's very frustrating that they don't really fit together
- safety and security - I'm really interested about provable programs, either dependent typing (Agda) or refined types (Liquid Haskell, ATS). Both require quite a bit of "static knowledge" - immutable data structures, or unique mutable data structures, and effect annotations for functions (plus, there are additional problems in lazy languages).
All of the above seem really hard to do using a dynamically typed language, but hopefully we can devise a way to have both a dynamic and a static provably efficient and secure code in the same program, same language, with clear split between the two.
- Dewie 12y ago> - memory usage - how should we handle deallocation - using reference counting with infrequent GC (Python) or by being very careful (C++), using just GC and allocating freely (OCaml/Haskell, Java & Nim use "realtime" GC), using uniqueness semantics (Rust, ATS), using memory pools and great care (Objective C) - none of these approaches is perfect and optimal for all situations, and it's very frustrating that they don't really fit together There is also ML Kit's usage of regions - I guess this is roughly the same std::Arena library in Rust.
- tel 12y agoTheorem proving doesn't require immutability it anything like that—its requirements are far more severe. Your language must have at least some fragment which is the internal proof language of a complete and consistent type theory! This is why, for instance, these languages are always Turing incomplete.
- tomp 12y agoHm... I'm not so sure about that. Of course, if we're speaking about dependent types, then yes. However, theorem proving could also be done automatically, by an external theorem prover, which would only need the refined type annotations on your variables to prove stuff (using the whatever theories the theorem prover knows about, such as linear integer mathematics, logic, real nonlinear math, vectors, datatypes, etc).
- tel 12y agoThat can happen sometimes for some theories. It's super easy to run into places where proof search fails magnificently.