> Dynamic languages, on the other hand, suffer from these drawbacks to a lesser extent, but they lack compile-time checks.

I.e. "The two or three popular dynamic programing languages I know don't have any compile-time checks".

Even my modest dialect (utterly not focused on type at all) Lisp can do a thing or two:

  1> (compile-toplevel '(let (x) (cons a)))
  ** expr-1:1: warning: unbound variable a
  ** expr-1:1: warning: cons: too few arguments: needs 2, given 1
  ** expr-1:1: warning: let: variable x unused
  #
  2> (compile-toplevel '(awk ((let (x y) (rng x y)) (prn))))
  ** expr-2:1: warning: rng: form x
                             is moved out of the apparent scope
                             and thus cannot refer to variables (x)
  ** expr-2:1: warning: rng: form y
                             is moved out of the apparent scope
                             and thus cannot refer to variables (y)
  ** expr-2:1: warning: unbound variable x
  ** expr-2:1: warning: unbound variable y
  ** expr-2:1: warning: let: variable y unused
  ** expr-2:1: warning: let: variable x unused
  #
  3> (compile-toplevel 'foo.bar)
  ** expr-3:1: warning: qref: bar isn't the name of a struct slot
  ** expr-3:1: warning: unbound variable foo
  #
Common Lisp implementations like SBCL have sophisticated type inference.

Dynamic programs can do things wrong in ways that are statically obvious.

You can catch the low hanging fruit, sure. But that ends up being pretty useless at scale, because your "checks" can't be relied upon. Or, worse, the programmer ends up having to understand the rules of your type system without having any way to probe or express the types of parts of their program, since your language is pretending that it doesn't have a type system.

That's only if you don't design your language to be easily inferred. While I don't know the case for SBCL, a language like Elm has very heavy type inference that you can rely on better than most type systems.

> While I don't know the case for SBCL, a language like Elm has very heavy type inference that you can rely on better than most type systems.

Bullshit. Either it's a sound type system (perhaps with some escape hatches) - in which case why would you ever not expose it as a real static type system - or it's not and you can't rely on it.

(There is no contradiction between having good inference and having a real static type system; e.g. if you're using Hindley-Milner then you have "perfect" type inference where you could remove all the type annotations from your program and it will still be correctly typed. But it's still very useful to have a syntax for annotating expressions with their types!)

Common Lisp is strongly typed, it's just that types follow values rather than bindings. This presents some code generation challenges, but it will warn on correctness just fine.

And of course if you really want an ML style BDSM type system in Common Lisp there's Coalton[1].

[1] https://github.com/coalton-lang/coalton