Programming Languages

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.


  • [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 []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


  • [MLang] :: A DSL created to represent and calculate the French tax code.
  • [Bloom]
  • [Dhall] :: langauge for system configuration
  • []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


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


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

, 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

[]-- book benjamin had, it's a description of term rewriting problems, universal algebra, unification theory

pl random link spit

[] -- overview of great works in pl to know before diving in!

[]-- software foundations

[] -- foundations in agda! for free!


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


[]-- run your research - talk on redex

[]a dsl for specifying and debugging operational semantics


[increasing the impact of pl research, connecting it to reality!]

[]:: 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... []

[What is your favourite academic paper on programming languages? : Programming...]: Cool papers to read!


[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.

2022-11-15 b60caae
2022-11-15 b99e7e7
2022-11-15 8db670e
2022-11-14 16da6fc
2022-11-14 cd752c4
2022-11-12 783744d
2022-11-11 fcaba77
2022-11-11 d08751e
2022-11-11 987384f
2022-11-03 340a00a
2022-11-03 7b0aae2
2022-11-03 1aa101d
2022-11-02 6c4b6ca
2022-11-02 5087026
2022-10-31 a3cd274
2022-10-31 076730e
2022-10-27 7836dc8
2022-10-27 95bda7c
2022-10-26 5bd8e25
2021-09-22 52a677b
2021-09-21 7732812
2021-09-03 84af9ea
2021-09-03 a43ac6a
2021-08-19 87d9551
2021-06-01 44926d9
2021-05-13 620c52a
2021-05-05 73a7cb9
2021-04-24 cdfa59c
2021-04-07 9d45dc4
2021-03-18 50772e2
2021-02-26 9ac6ea5
2021-01-20 6a70d3f
2021-01-20 35e386e
2021-01-19 4e62c15
2021-01-18 af0b1e0
2021-01-17 675fddc
2021-01-15 d1b02d2
2021-01-15 4cf5fb9
2021-01-15 cccf2d4
2021-01-15 1c39319
2021-01-15 f2197ab
2021-01-15 5599273
2021-01-15 446991d
2021-01-05 c564d7c
2020-11-29 16b87cc
2020-11-26 ce5cd9c
2020-11-25 e68d56d
2020-11-23 5857d9d
2020-11-23 d83a5ed
2020-11-17 fb0d822
2020-11-15 a0eccac