It depends on how you implement the gradual typing as well. Through contracts is one way (probably the bad way, since they still apply at runtime) and static analysis with type annotations is another way. There isn't any reason a sufficient static analyzer couldn't be as powerful as an inbuilt static type system.

This is effectively dragging some of the benefits of static typing to dynamic typing. I wonder why you'd pay the cost of dynamic types though, instead of going the other direction. With type inference you don't need to explicitly write types the entire codebase, and you can opt-in to dynamic types in controlled, explicit scenarios.

Parsing and generative testing are well-covered by static types, but I'll give you that contracts can enforcing things static types cannot. That said, static types can enforce things that contracts cannot, too.

Furthermore, in my experience I find use of the things that static types can catch and contracts cannot on a nearly hourly basis while I rarely to never use things that contracts can check but static types cannot.

> Immensely powerful abstraction

Let's take a look.

> Validation

Validation typically means that given a set of shapes of data from a large class we should determine whether a certain instance fits within a smaller class. For instance, parsing selects out valid strings amongst all strings.

Haskell has a number of libraries like this. Let's use JSON for example. We create instances of the typeclass

    class FromJSON a where
      parseJSON :: JSON -> Maybe a -- simlplified

and now each type which instantiates that class gets an automatic validation as a JSON-like type. Similar patterns are available for any other kind of "validation".

> Coercion

Coercion in the core.spec sense is a similar game to the kind of enhanced validation I used above. If validation picks out a subset of valid instances, coercion, conformance, lets more than just the subset stand for itself—other instances can "conform" to the same thing.

Again, type systems are very handy for this. The JSON example above is already taking care of this in a way more robust than core.spec. The desired result type `a` drives all possible "parses" and conforms them all to its value.

> Error reporting

Let's take a closer look at a more real type of the method within FromJSON

    class FromJSON a where
      fromJSON :: JSON -> Validation ParseError a

what a `Validation` does is collect errors which occur in the parsing of a value `a`. All of the errors which arise throughout parsing are collected.

Now, core.spec takes advantage of Clojure's core data language (EDN or whatever) which has the property of having concrete "paths" from the root of any value down to any sub-value within it. This is a nice property in that core.spec can pinpoint the location of an error within a type.

But it's a property of the shapes of Clojure data, not a property of Spec. We can write a type in, e.g., Haskell, which has the same properties. If we replaced JSON with that type then we'd have the exact same property.

> Automated test generation

This one makes me laugh a little bit. Automatic test generation was invented for use in Haskell's type system. For this we have the typeclass

    class Arbitrary a where
      arbitrary :: Gen a

where `Gen` denotes a randomly chosen value which can be "shrunk" to find a more minimal example. Create a collection of Arbitrary instances for the data of your system and you'll immediately be able to generate "property tests".

Reid Draper, original author of test.check, actually was cribbing the design precisely from Haskell's QuickCheck library.

---

So we might wish our types did these things... But we'd be mistaken to do so. Our types already do these things and have for longer than Clojure has been around!

Furthermore, I really can't let it pass that Clojure's core.spec is not a form of static typing at all. It enables no guarantees at compile time, only at runtime.

Core.typed is a static type system and is outside of the compiler as you note, but there's nothing special here. People put type systems in their compilers for (a) convenience and (b) to guarantee the things fed to the compiler are well-typed so that the compiler can generate more efficient artifacts. Both of those reasons are auxiliary, optional. There has never been a reason why a language couldn't just build an external type-checker. Hell, Flow and TypeScript are more or less exactly that.

Sorry to come on strong, but I think it's quite far from the truth to take these things as benefits of dynamism. They have always been there. Dynamic languages just make them a little harder to access.

People vote with their feet, and while I'm really sympathetic to everything you're saying about static typing, it's hard to argue that reality is producing a lot of really popular dynamically typed languages. JS being exhibit #1, but also python, ruby, clojure, and on and on.

Take a look at how fast javascript mutates, I'd argue that rate of mutation is one of the things you can do in a dynamically typed language. Java doesn't mutate like that, despite having many of the same ecosystem pressures, such as the pressure to "be good at everything" because it's so widely used.

That mutation often comes with unneeded parts and kludges, but the rate of mutation and change in the JS ecosystem has also been a huge positive. Still, TANSTAAFL and all that, I'm certainly not saying it's all good -- but I think you overstate it considerably when you say "A lot to lose and nothing to gain with dynamic typing"

Given the rise of transpilers targeting JavaScript, "stuck with javascript" doesn't mean quite as much as it may have in the past. You could argue that this is "bolted on", but given the current state of tooling and how quickly it's improving, I don't think it's a fair characterization. I suspect this trend will only continue.

If it's as simple as "javascript because web" as you suggest, how does that jibe with things like Electron (js desktop apps) and back-end JS without a web facing component? None of those people had to pick JS.

WASM will be here soon, and from that point on we can elegantly compile from any language to the browser platform.