4 ms·

In my experience, people believe that programming languages are a solved space, and we should stick with what we have. It's an unfortunate view. Languages are

In my experience, people believe that programming languages are a solved space, and we should stick with what we have. It's an unfortunate view. Languages are actually very polarized today. I think there's a lot of room for a mainstream language that could be safe, fast, and most importantly, easy. Today's languages are generally two out of three. Luckily, a lot of languages are exploring that space! * Vale is blending generational references with regions, to have memory-safe single ownership without garbage collection or a borrow checker. [0] * Cone is adding a borrow checker on top of GC, RC, single ownership, and even custom user allocators. [1] * Lobster found a way to add borrow-checker-like static analysis to reference counting. [2] * HVM is using borrowing and cloning under the hood to make pure functional programming ridiculously fast. [3] * Ante is using lifetime inference and algebraic effects to make programs faster and more flexible. [4] * D is adding a borrow checker! [5] [0] https://vale.dev/ https://vale.dev/ [1] https://cone.jondgoodwin.com/ https://cone.jondgoodwin.com/ [2] https://www.strlen.com/lobster/ https://www.strlen.com/lobster/ [3] https://github.com/Kindelia/HVM https://github.com/Kindelia/HVM [4] https://antelang.org/ https://antelang.org/ [5] https://dlang.org/blog/2022/06/21/dip1000-memory-safety-in-a-modern-system-programming-language-pt-1/ https://dlang.org/blog/2022/06/21/dip1000-memory-safety-in-a...

alexisread 4y ago
I suppose you could add a few to this list: Koka has formalised side-effects, and thanks to that can do in-place mutation after static analysis, similar to HVM. It also uses static analysis to manage memory with elided reference counting. Lastly, koka has managed to utilise static typing with dynamic binding, contrast with cell-lang which avoids dynamic binding (which has it's use cases). https://koka-lang.github.io/koka/doc/book.html#sec-effect-types https://koka-lang.github.io/koka/doc/book.html#sec-effect-ty... Flix does something similar to cell, though the typing is worked out better as lattice types ensure that there is an unambiguous top and bottom type. Addditionally where cell cannot compute dependent values, Flix can as it uses constraint modelling rather than reactive computation ie. the algo computing the rules is formally worked out to cover the edge cases. https://flix.dev/principles/ https://flix.dev/principles/ Maude handles subtyping and typechecking of said subtypes through equational and rewrite logic. It has the concept of purely functional modules as well as impure (system) modules, but adds to that the math theories that represent the modules, so you get a lot of formal verification techniques at your disposal while programming. http://maude.cs.illinois.edu/w/index.php/Maude_Overview http://maude.cs.illinois.edu/w/index.php/Maude_Overview Composita covers the idea of removing pointers, and restricting components so you can use concurrency in anger (and managed memory without GC at the component level) https://concurrency.ch/Content/publications/Blaeser_Component_Operating_System_PLOS_2007.pdf https://concurrency.ch/Content/publications/Blaeser_Componen... Kali makes a good job of migrating processes - where cell restricts the ability to do closures due to the extended value set, kali can walk the call tree to migrate all linked state. http://community.schemewiki.org/?Kali-Scheme-Revival http://community.schemewiki.org/?Kali-Scheme-Revival I think cell looks interesting, but there seem to be restrictions here to simplify/avoid some of the harder problems. That in itself is not a bad thing, but it's worth noting given that some of these problems have been tackled individually above. I'm not quite ready with a blend of these techniques, but it looks as though they are compatible with each other.
- verdagon 4y ago
  Wow, I've never heard of most of these languages, and I consider myself a language expert! How did you learn of these?
  - alexisread 4y ago
    Mainly reading threads here :) I make a stab at looking at the top headlines. There's a pattern in a headline eg. Mentions of GC, datalog and so on which I flag. The exceptions are Composita and Maude. Composita is off the back of Oberon, which is one of the smaller language-based OSes. Maude I found on a keyword search around formal verification- I'm looking to build a new language so interesting stuff keeps coming up when you go down the rabbit holes ;)
avgcorrection 4y ago
Languages are not that polarized. Most languages are in fact compromises, design-wise, rather than very principled (polarized). Rust[1] and ATS are the only no-compromise newish (this century) languages that are very principled. (EDIT: in the high-level with low-level control category.) Being supposedly easier is also easier (design-wise) than being principled, since you are able to compromise on whatever dimension (like e.g. memory safety) as long as you make things just a bit easier than the competition.[2] A language like Rust, on the other hand, has to (1) make Safe Rust memory safe and (2) make make it possible to create Safe Rust APIs using Unsafe Rust. Polarized design is the road less travelled. [1] All your examples mention “borrow checker”… [2] For propaganda purposes, a subjective criteria like “easier to use” (than e.g. Rust, if that is applicable) is better than a technical criteria like being memory safe.

alexisread 4y ago

I suppose you could add a few to this list: Koka has formalised side-effects, and thanks to that can do in-place mutation after static analysis, similar to HVM. It also uses static analysis to manage memory with elided reference counting. Lastly, koka has managed to utilise static typing with dynamic binding, contrast with cell-lang which avoids dynamic binding (which has it's use cases). https://koka-lang.github.io/koka/doc/book.html#sec-effect-types https://koka-lang.github.io/koka/doc/book.html#sec-effect-ty... Flix does something similar to cell, though the typing is worked out better as lattice types ensure that there is an unambiguous top and bottom type. Addditionally where cell cannot compute dependent values, Flix can as it uses constraint modelling rather than reactive computation ie. the algo computing the rules is formally worked out to cover the edge cases. https://flix.dev/principles/ https://flix.dev/principles/ Maude handles subtyping and typechecking of said subtypes through equational and rewrite logic. It has the concept of purely functional modules as well as impure (system) modules, but adds to that the math theories that represent the modules, so you get a lot of formal verification techniques at your disposal while programming. http://maude.cs.illinois.edu/w/index.php/Maude_Overview http://maude.cs.illinois.edu/w/index.php/Maude_Overview Composita covers the idea of removing pointers, and restricting components so you can use concurrency in anger (and managed memory without GC at the component level) https://concurrency.ch/Content/publications/Blaeser_Component_Operating_System_PLOS_2007.pdf https://concurrency.ch/Content/publications/Blaeser_Componen... Kali makes a good job of migrating processes - where cell restricts the ability to do closures due to the extended value set, kali can walk the call tree to migrate all linked state. http://community.schemewiki.org/?Kali-Scheme-Revival http://community.schemewiki.org/?Kali-Scheme-Revival I think cell looks interesting, but there seem to be restrictions here to simplify/avoid some of the harder problems. That in itself is not a bad thing, but it's worth noting given that some of these problems have been tackled individually above. I'm not quite ready with a blend of these techniques, but it looks as though they are compatible with each other.

verdagon 4y ago
Wow, I've never heard of most of these languages, and I consider myself a language expert! How did you learn of these?
- alexisread 4y ago
  Mainly reading threads here :) I make a stab at looking at the top headlines. There's a pattern in a headline eg. Mentions of GC, datalog and so on which I flag. The exceptions are Composita and Maude. Composita is off the back of Oberon, which is one of the smaller language-based OSes. Maude I found on a keyword search around formal verification- I'm looking to build a new language so interesting stuff keeps coming up when you go down the rabbit holes ;)

avgcorrection 4y ago

Languages are not that polarized. Most languages are in fact compromises, design-wise, rather than very principled (polarized). Rust[1] and ATS are the only no-compromise newish (this century) languages that are very principled. (EDIT: in the high-level with low-level control category.) Being supposedly easier is also easier (design-wise) than being principled, since you are able to compromise on whatever dimension (like e.g. memory safety) as long as you make things just a bit easier than the competition.[2] A language like Rust, on the other hand, has to (1) make Safe Rust memory safe and (2) make make it possible to create Safe Rust APIs using Unsafe Rust. Polarized design is the road less travelled. [1] All your examples mention “borrow checker”… [2] For propaganda purposes, a subjective criteria like “easier to use” (than e.g. Rust, if that is applicable) is better than a technical criteria like being memory safe.