[tluyben2]

Idris and Coq which have more advanced type systems allowing you to create proofs for you software. There are not many languages that allow this.

And Shen which has a Turing complete type system meaning it is very flexible but type checking may never halt in certain conditions. I do not know of another language with these properties.

Haxe allows you to target absolutely anything and if you miss some exotic it is trivial to allow generation for it. It is also quite mature language with a macro system. Again, maybe MonkeyX compares somewhat but has far less backends and making a backend is not so straightforward.

K and Q and their parent APL which allow you to write the most terse code you will ever see (some make a sport of it).

Forth you can implement in a few hours on any platform and yet is a very powerful language which makes it easy, once you get used to it, to write terse but easy to understand code. This one I would say is, compared to other languages including Lisp, easier to implement naively while still keeping solid perf. There are also lists of minimal instruction Forths which show you how powerful and easy the basic constructs are and how rapidly you can make a toy language.