Why static languages suffer from complexity

I was under the impression that it's substantially an implementation of an affine type system (https://en.m.wikipedia.org/wiki/Substructural_type_system).

Probably you could build such a thing without thinking about types per-se, but I don't think the designers of Rust did that, and I am not sure that makes it "not a type system" anyway.

> any static analyzer is a type system

"Any static analysis checking correctness is either a linter or a type checker" isn't a claim I would make, but I am not sure offhand how I would argue against it.

It "can", but it's a design decision not to by default because mixing `uint` and `int` is usually a bad idea.

This is telling the compiler you want to add an `int` that represents (say) 63 bits of data with a +/- sign bit to a `uint` that doesn't have a sign bit. If `a = -1` then `b = uint(a)` leaves `b == 18446744073709551615`. Is that expected? Is it a bad idea? Yes. So, the explicit casting is "getting in your way" deliberately so you don't make these mistakes. If `a` is a `uint`, it can't be set to `-1`, and adding them is freely allowed.

Incidentally `uint` shouldn't be used for other reasons too, for instance unsigned integers wrap around on overflow, whereas integers raise overflow errors. The freedom of mixing types like this are why languages like C have so many footguns.

In short, explicit is better than implicit when data semantics are different. When the semantics are the same, like with two `int` values, there's no need to do this extra step.

You could create a converter to automatically convert between these types, but you should know what you're doing; the compiler is trying to save you from surprises. For `int`/`float`, there is the lenientops module: https://nim-lang.org/docs/lenientops.html. This has to be deliberately imported so you're making a conscious choice to allow mixing these types.

> don't you get tired of typing (and reading) `uint` twice in the latter setting?

Well, no because I wouldn't be writing this code. This example is purely to show how the typing system lets you write pythonesque code with inferred typing for sensible things, and ensures you're explicit for less sensible things.

For just `int`, there's no need to coerce types:

    var
      a = 1
      b = a + 2
      intro = "My name is "
      name = "Foo"
      greeting = ""

    b *= 10

    # Error: type mismatch: can't concatenate a string with the `b` int.
    # greeting = intro & name & " and I am " & b & " years old"

    # The `$` operator converts the `b` int to a string.
    greeting = intro & name & " and I am " & $b & " years old"

    # If we wanted, we could allow this with a proc:
    proc `&`(s: string, b: int): string = s & $b

    # Now this works.
    greeting = intro & name & " and I am " & b & " years old"

    echo greeting # "My name is Foo and I am 30 years old"

    # Normally, however, we'd probably be using the built in strformat.
    # Incidentally, this is similar to the printf macro mentioned in the article.

    import strformat
    echo &"My name is {name} and I am {b} years old"

I feel that is much too pessimistic.

>will only cover a small case of the actual specification.

If the same applies to proofs: so be it. Don't let perfect be the enemy of good!

>For example I would bet money that not a single function in the C, C++, Java and Python standard libraries is fully specified, in the sense of nailing down the program up to observational equivalence.

I'd imagine so as well, but I think that's more indicative of how even a (superficially) simple language like C is not all that amenable to specification.

> A lot of code refactoring I've done was trivial (e.g. changing the order or arguments), but ripples through the program and proof structure.

This is not my experience. If you use sufficient proof automation, something like this should have next to no impact on proof structure. Univalence is useful, but a lot of refactoring is not just switching to isomorphic representations, so I'm convinced that larger scale proof automation is way more essential than HoTT.

> Java exception specifications

I'm not convinced that this is fundamental to specifying exceptions rather than just Java having particularly poor ergonomics for it. I've never met a person that actually liked implicit exceptions and if you ask people who dislike exceptions, that's often one key part of it.

> In contrast, expressive type-theories constantly force you to prove a lot of trivialities.

For all large dependently typed languages that actually bill themselves as programming languages (Agda, Idris, Lean) there is some sort of 'unsafe' feature that allows you to turn the termination checker off - at your own peril of course. But you only pay for what you use, if you don't need the additional correctness, you don't need to put in any more work, just like with unit tests.

(There are also ways to safely defer termination proofs, but to be fair the experience isn't the best currently.)

>I don't know what you mean by declarative (other than: leaving out some detail).

Specs tell you the what but not (necessarily) the how. Take the spec for all sorting algorithms (giving observational equivalence):

1. The output list is a permutation of the input

2. The output is sorted in regards to some predicate.

That's a couple lines at most (or a one-liner if you don't count the building blocks like the definition of a permutation), which is a good amount shorter and easier to verify than e.g. a full heapsort implementation.

>But they cannot be smaller in general: if every program P had a full specification S that was shorter [...] then you've an impossibly strong compressor

The compression is stripping away the 'how', that's why you can't 'write a spec for a spec' and compress further.

>What you see in practise is that you only specify some properties of the program you are working on.

Sure, writing a fully specified program of non-trivial size is currently really only possible if you're willing to ~waste~ invest a decade or more.

>Moreover, if you only work with a partial specification, you can ask the question: what level of partiality in my specification gives me the best software engineering results.

Why would you assume that there is a single level of partiality that gives the best results? I agree that HM style types are a great fit for 'general' programming because it has such low impedance, however I also believe that most programs have some areas where they would benefit from more specification. (I think people have a clear desire for this and that it's at least partially responsible for some of the crazy type hackery as seen in Haskell or Scala, which could often be greatly simplified with a richer type system.)

Having a richer type system doesn't mean that you always have to fully use it. It's perfectly possible to just use a HM style/System F fragment. Using dependent types just for refinement is already one of the dominant styles for verification. If dependent types ever become mainstream in any way, I imagine it will also be largely in that style.

    let b: uint = uint(a)

    # can be written as:
    let b = uint(a)

    let b: uint = a

    let b = a