TLDR: I've explored tons of languages, but ultimately I think that Zig (systems) and Common Lisp (general purpose) (relatively soon: my own Lisp, TBD) are worth betting on, my criteria being:

• Performant. Racket, Clojure and other lisps are slow relative to Common Lisp. I don't have time for a slow programming language built on some hill of abstractions when high level languages that are also incredibly fast exist.
• Fast to use. I don't want to have to learn new language features. I should be able to get from 0 to product as easily as possible.

Languages

J
A high-performance language for data processing and parallel computing. J implementation in Nim. it has a different mental model of programming languages reading hillel wayne essay on it is cool! can create a unique sieve as a value and make assignmetns! can transform the object directly after it has been created! j provides mechanism to fuse mapping and filtering, can study properties of the sieve https://github.com/pitr/jj: J implementations in C and C++, Rust

Fractran
XXIIVV — fractran . Cool?

Z
A dialect for C that's immutable by default, resolves undefined behavior and uses an SMT solver to guarantee reference stability

Chapel
A parallel programming language that claims to have some novel ideas.

Catala
A DSL for representing laws by construction, designed to enable lawyers to certify laws. Interested in formal verification of legal documents, potentially.

Raku
A descendent of Perl, it features lots of additional features including fun grammar specifications.

Ante
'The compile-time language'. Made by a Northeastern undergraduate.

Oak
Designed as a simple replacement for C.

Topshell
A functional, reactive scripting language.

Chef
An esoteric programming language designed to simultaneously represent recipes and programs.

Whitespace
A programming language designed with only whitespace characters, ignoring all others. Any program that disregards whitespace can express a whitespace program within it. Fun to represent in laugnages that aren't indent-aware - these programs can also encode Whitespace within them!

Lux
A statically typed Lisp-like language for the JVM.

While
A language used in textbooks such as 'Principles of Program Analysis'.

PolyRPC
A 'multi-tier' functional programming language.

Steno
livecoding metalanguage

Unlambda
A minimal functional programming language based on combinatory logic meant to be a demonstration of pure functional programming

Vodka
A creative coding environment and language for structured editing for writers.

Play
A statically typed Forth!

Imba
A programming language for the web that finally handles full stack in all of the right waysLove the syntax!!! Great lessons from someone who knows how to teach as well - very easy to understand and get started with the language!

Smalltalk
Innovative "talk to objects" approach! Self (programming language) - Wikipedia is an evolution of this. Why is self interesting independent of smalltalk? Not sure?

Faust
Programming language for signal processing! Super fast super super fast. I wonder if any of these ideas and principles can be implemented in some DSL used in Rust, Hasnekk, Zig, etc…

Piet
DM's Esoteric Programming Languages - Piet: A cool programming language in 2D leveraging solid colors and art cycles!

The Nomsu Programming Language – Nomsu
A cute programming language that stays as close as possible to natural language. A function definition conveys some statement in natural language - it's a phrase that can parse some argument(s) provided anywhere in the phrase - and allows users to write in more clear English. It's a fun idea, but I doubt that this system preserves its readability when working with complex programs; I'd bet that it approaches the complexity of a large, mathematical proof and takes on the structure of a programming language but far more verbose and a bit more difficult to reason about (Assume we have some variable that meets this constraint; set it here, reset it here, apply this function composition here, and so forth). It's possible that there is some way to escape this - but I've only spent five minutes reading this thing.

Flix | The Flix Programming Language
Cooooooool

DSLs

MLang
A DSL created to represent and calculate the French tax code.

• Bloom
• Dhall :: langauge for system configuration
• https://microformats.io/ html dsl in classes to add meaning
• puzzlescript :: language for puzzles!
• Frink :: The Frink is Good, the Unit is Evil. Language that's optimized for unit conversions and usability; if I have to do a lot of unit manipulation and I'm worried about forgetting anything, I can offset the burden to Frink and mostly use it like a super elegant calculator. No problem. The local optimum of embedding such a system in a language with ADTs seems better though, honestly…
• Alda :: Make music!
• Unison :: A distributed programming language and editing environment for the modern web. A major inspiration for the projectional Text Editors project.
• Inform 7 :: A programming language for expressing interactive fiction. The source code is published as an expressive literate program that's navigable through the website - it's super interesting! This is downstream from some choose your own adventure system but seems far more expressive… there seems to be a community that gathers monthly at MIT to discuss these things: The People's Republic of Interactive Fiction - Play. Might be worth visiting in January : )

blurring the curry howard line

source works on autonomous vehicles, fun stuff.

typically using languages iwth proof assistants. however, actuation systems in carshave real time constraints, so lazy evaluation or nondeterministic memory management is not valid. this is typically done in c or cpp. pulling a c program from a coq proof ?

programs :: formalized syntactically but modeled semantically. denotational semantics map some number to some set :: ie some u8 integer fits within one set. map syntactic objects to universal mathematics with such denotational semantics.

typing rules: tau - a : A, f:A -> B

tau |- a

cannot capture everything with type theory? dependent types end up capturing everything. can provide complete specification of a program's behavior in the dependent type theory.

curry-howard correspondance :: a correspondence between program and proof! we know we can reason about our programs from a dependent type theory, but what is this gap called? specifying program in the types: can make assertions about the correctness of this code.

why dependent types matter paper. rust provides subset for representing dependent typed behavior in our programs. type level definition of the natural numbers, for example!

these programs can be fully represented in state machines! the entire system and communication protocols can be captured with such a state machine, and this state machine can be represented in a rust type system.

state :: sum type. type family adjacency; types that are members of the type family are adjacent to each of these states.

can use demotational semantics to convert rust semantics to agda :: and as agda has full dependent types. using agda allows us to mechanize semantic function ! agda has a notion of proofs and may soon have a notion of tactics. proving things foundationally in agda could be doable once we have the specification of the program in its own domain

state machines :: behold the program counter as everything is tracked at compile time. not easy in this representation to track a state machine in terms of program handlers.

church numerals :: general way of using a function to produce numbers program that extracts information from a rust program and stick the semantics in agda

Lua

Really interesting, compact language with lots of work developing sub-languages.

Fennel
Lisp for Lua.

Terra
A metaprogramming language that lets you metaprogram with and in the language! Looks like Ebb is a language embedded in Terra for easily using physical simulations, embedding meshes and such. Not sure when I'll ever use this, but it's a testament to the power of this Terra system…

Experimental langauges…

Effekt Language: Home: Has effect polymorphism and handlers. Effect safety. Extempore documentation: Why do I have this saved? Might be interesting.. The reflective language Black: A Scheme extended with the function `exec-at-metalevel`, a function that allows arbitrary access and modification to the metalevel interpreter, modifying the semantics of the language from within the language itself. 10 Most(ly dead) Influential Programming Languages • Hillel Wayne: An overview of influential programming languages and their details.

Z: This is really cool… most of the innovation is in the concrete syntax, sure, but the fact that the new indentation and super simple function application without parens works means that macros are far more powerful. Concrete syntax makes things more readable, and doing things like defining a comment with a macro advances text! It's a cool idea. You'll probably end up tripping up fairly fast though… definitely a bit of a toy. Also notable that it's kind of just lisp without parens and some cute re-parsing trick / re-eval at macro time that allows for some more elegant concrete syntax.

future reading

Great Works in Programming Languages: An overview from Benjamin Pierce of great programming language works throughout history - direction for what's worth reading and worth knowing.

term rewriting

https://www21.in.tum.de/~nipkow/TRaAT/ – book benjamin had, it's a description of term rewriting problems, universal algebra, unification theory

pl random link spit

https://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml – overview of great works in pl to know before diving in! https://softwarefoundations.cis.upenn.edu/ – software foundations https://plfa.github.io/ – foundations in agda! for free!

parsing

shunting yard algorithm : used to parse expressions in infix notation !

redex

https://www.youtube.com/watch?v=BuCRToctmw0 – run your research - talk on redex https://redex.racket-lang.org/ a dsl for specifying and debugging operational semantics

meta

increasing the impact of pl research, connecting it to reality! http://www.is.ocha.ac.jp/~asai/Black/ :: an extension of scheme that not only allows for metaprogramming, but also meta-modification of the interpreter it's running on! any program can modify the behavior of the interpreter. nuts! interview about unlambda Probabilistic Programming is a brilliant overview of the space from a major contributor, Adrian Sampson. Jean Yang on An Axiomatic Basis for Computer Programming - YouTube What are some interesting language features that may not be well known? : Pro…: Cool language features? In Further Praise of Dependent Types | The n-Category Café: Lol someone likes dependent types…https://golem.ph.utexas.edu/category/2020/05/in_further_praise_of_dependent.html What is your favourite academic paper on programming languages? : Programming…: Cool papers to read!

Parsing

Which Parsing Approach? | Hacker News: An "LL" recursive-descent parser (recursive descent can handle an LL grammar) is the best way to go because it provides the best error messages.