100% Test Coverage means that every code path is executed by the test suite. This is probably a good thing.

Yet it does not mean that the code is correct for any definition of "correct" other than "passes the associated test suite." One unit test makes a line of code covered. It does not make the domain of inputs covered - 100% coverage does not mean that corner cases have been handled correctly - or that they have been considered at all. Again, all it means is that every line of code was executed at least once.

There are useless tests:

     def test167  [
       if [ val == foo(8); return true]
         then return passed
         else return failed
       endif ]
     enddef

This of course is true. But some test coverage tools with give you path coverage which helps with that.

Of course, this doesn't really substitute for a type system either.

It can be very costly to achieve 100% test coverage and static verification can reduce this cost by giving you some tests "for free". For example, you never need to write a test to check for null-pointer-exceptions if you code in Haskell.

Static types also help in situations other than testing. For example, you can use "guardrail programming" to be much more liberal when refactoring things: want to change a function signature? Just change it and the compiler will point out what other parts of the code need to be updated. This is even if you haven't written a test suite yet or are doing big changes that invalidate the old test suite.

That said, I think the perfect world would be one that lets you mix dynamic and static typing in a single program (some things are hard to verify statically, but would be nice if we could at least express them as types) but I think we are still a way off that being a practical alternative.

I know in C# they have the dynamic keyword which allows for dynamic typing when you need it, but lets you use static typing when you don't.

Yes, C# and lots of other language have that feature. Where it gets really tricky is if you want to dynamically check the type of functions or objects, since you need to run the assertions when the function/method gets called rather than when the function/method gets assigned to some reference. Its also tricky to give a parametric type to code that is implemented with dynamic types.

I'm not convinced that requiring test coverage is a good trade off.

Don't misunderstand me: tests are good. But language syntax that makes some bugs impossible is also good.

The cognition overhead of 100% test coverage is probably absurd, as well.

Probably you are right, but for a library I think it should be an obligation to provide 100% coverage. For a generic program, maybe I sould provide 100% coverage at least of the "critical paths".

Might also be worth it to emphasize the "intended paths."

Of course, that is probably just saying that there should be documentation.

Especially given that you can't reasonably enforce the rigor of your test suite by way of your language.

Oddly, you could, in a way. Just treat your language and compiler as a tool in the toolchain. Add in a testing segment and you can set rules on it.

I still don't understand the notion that dynamic types gives you anything more than static types. Are there really usefull programs that can't be written in, say, Haskell?

IMO, its not just about what useful programs you can write. Its also about how much of the type system you need to learn to get the program to compile. For example:

    function foo(f){
        return [f(["1", "2", "3"]),  f([1,2,3])];
    }

    function length(xs){
        return xs.length;
    }

    foo(length);

Anyone can see what this Javascript program doing but to write the Haskell equivalent you would need to understand higher-rank-types and enable the corresponding language extension, which gets in the way of beginners.

Unfortunately I do not know so well Haskell to give you an answer. I was referring to this:

> I think this is because there is yet to be a language that makes expressing complex types easy.

Since I'm obliged to use a dynamic language (JavaScript) I'm looking for a solution in it. And in JavaScript is really easy to express a complex type, say "the set of all the even integers between 2 and 14 but 10", using runtime checking to enforce the constraints. Is it simple in Haskell to define such a set in its type system?

Simple? Yes. Pleasant? Not really. I'm not a Haskell expert but I can write that type in Scala (the Haskell version probably has less boilerplate, but still some):

    sealed trait Even[N <: Nat]
    object Even {
      implicit object zero extends Even[_0]
      implicit def evenSS[N <: Nat](implicit e: Even[N]) = new Even[S[S[N]]]{}
    }
    sealed trait EvenAndBetweenTwoAndFourteenAndNotTen
    object EvenAndBetweenTwoAndFourteenAndNotTen {
      implicit def forN[N <: Nat](implicit e: Even[N], le2: Le[_2, N], le14: Le[N, _14]) =
        new EvenAndBetweenTwoAndFourteenAndNotTen[N]{}
      implicit object interfere10 extends EvenAndBetweenTwoAndFourteenAndTen[_10]
    }

Like I said, it's cumbersome, but there's nothing actually complicated about writing this, it's just boilerplate to represent it in the type system.

On the other hand, in Idris or the other languages mentioned in the article, you should be able to write that kind of constraint at the type level just as easily as you can at the value level. That's where it gets really exciting.

In javascript, any method that relies on receiving a value of "the set of all the even integers between 2 and 14 but 10" should probably check that it did in fact receive such a thing or it might be buggy. In a statically typed language, that check can easily be centralized to wherever an `EvensFrom2To14Without10` value is constructed.

Here's an example in rust[0]. If the `print_bare` method relies on only receiving even numbers between 2 and 14 excluding 10, then it is buggy, because it isn't checking its input, but the `print_tagged` method is correct without needing to check!

[0]: http://is.gd/9uHrc7

That's not really expressing a complex type in JavaScript, its expressing a complex (such as it is) runtime constraint -- which you can do easily in Haskell as well. JS doesn't give you anything Haskell doesn't there.

Its true that to make that a proper, statically-enforced type in Haskell takes some complexity, but if you aren't willing to do that, you could make it a runtime-enforced constraint on a statically-enforced type of integers as easily in Haskell as, in JavaScript, you could make it a runtime-enforced constraint on a value that is not statically enforced to be anything more specifically than a valid JS value.

I do not know Haskell enough either. But I didn't really mean 'using type system everywhere'. About your question, from what I've seen you can always go symbolic : define an abstract thing as twofourteenexceptten that represent that idea and use it. Or just use a filter everywhere to ensure that function requiring a 2and14but10 won't be called on something with other numbers. In that case you're not losing anything you'd do with a dynamic language.