Just as a little addendum to that: The theory of statically typed languages[1] is progressing while "dynamic" languages haven't actually had many real advances

Just as a little addendum to that: The theory of statically typed languages[1] is progressing while "dynamic" languages haven't actually had many real advances since e.g. Scheme[0] first appeared. Sure, there's small things around ergonomics, immutability (Clojure, especially), but really there's been very little true advancement[2]. Personally, I think either static (dependent) types will win[3] or we'll just end up implementing different custom static type systems ad-hoc[4]. My reason for having more confidence in the former rather than even more formal methods is that there are very few math-like/truly spec-level languages (e.g. TLA+) that can be mechanically translated to a meaningful program. We need something intermediate, but so far (to me!) Idris[5] has seemed like the only remotely credible contender in that you can pretty much choose arbitrarily how much provin' vs. how much assumin' you want to do. EDIT: The current hype (in frontend especially) seems to be around 'gradually typed' languages like TS and Flow, but AFAICT they are basically just a very poor man's ad-hoc version of dependently typed languages. (Concretely TS/Flow do have a huge advantages in that it's really easy to introduce, but personally I had no problem transitioning gradually from ES6/traceur to Scala.Js/React just by adding strongly typed shims where appropriate. If your application is so tangled that you cannot introduce such shims in various places, it's probably tangled enough that you'll want to do a full rewrite anyway.) [0] I think Scheme was the first to introduce first-class continuations. That was a pretty major advance in terms of expressing, for example, search algorithms by just rewinding to a previous continuation. Of course, since then "we"(Felleisen, specifically) discovered that delimited continuations are perhaps better -- but that was a 'refinement'. [1] Aka: languages with more than one type. [2] Of course, some might interpret (pun!) that as a sign that they're "perfect". However, we still get loads of bugs in dynamically typed languages, so surely there must be something to be improved upon, right? [3] See e.g. "State Machines All The Way Down" at https://eb.host.cs.st-andrews.ac.uk/drafts/states-all-the-way.pdf https://eb.host.cs.st-andrews.ac.uk/drafts/states-all-the-wa... (DRAFT) [4] See e.g. "Type systems as macros" at http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf (DRAFT) [5] Since I'm already thowing around references, I'd also point to the "Elaborator Reflection" paper; PDF at http://davidchristiansen.dk/drafts/elab-reflection-draft.pdf http://davidchristiansen.dk/drafts/elab-reflection-draft.pdf ; video at https://www.youtube.com/watch?v=pqFgYCdiYz4 https://www.youtube.com/watch?v=pqFgYCdiYz4 . It shows just how much provin' you can do with just a little bit of ad-hocness at compile time.