1. It's a tooling artefact, testing systems certainly don't have to mandate split code and tests. Rust's test framework allows tests in the same file as the tested code, the testing guide recommends that unit test live alongside the code they test[0] and the standard library follows this practice[1]. I'm reasonably sure you can also do so in e.g. py.test[2]

2. I'm not convinced editing two files slows you down, most editors and window managers will let you put both files side-by-side and trivially jump between them. Are java developers slowed down by having to jump between files?

[0] http://doc.rust-lang.org/guide-testing.html#the-test-module

[1] https://github.com/rust-lang/rust/blob/4deb27e/src/libcollec...

[2] by marking all python files as "test modules"

OP is referring to this line:

It also turns out, in both softwares, a majority of the couplings are attributable to Test Driven Design, where a source code is coupled to its test. So these are apparently false-positives I should take care of in the next version of the pipeline.

Not shown: the part where the critical production bug you introduced was caught by your test suite, thus saving you countless hours of agony, angry customers, and lost revenue.

It works both ways, and probably one of the biggest skills to being an effective developer is understanding whether a piece of code you write is likely to be thrown away shortly or whether it's going to live forever and cause umpteen headaches for the maintainer. (This itself is surprisingly counterintuitive: I have seen high-priority code backed directly by an executive thrown away a week after being written because of shifting perspectives within the organization, and I've also seen a one-character typo in a "throwaway" migration script result in restoring a million+ users from tape backup.)

By all means do leverage your type system as much as you can, avoid writing tests for what you know your type system handles, and (if your type system is expressive enough) use property-based testing to further leverage your type system into essentially fuzzing your functions.

But you'll still need to write tests.

How on earth do you write a type, or set of types, for that that actually bear some resemblance to the spec and don't simply reflect the details of the implementation?

To simplify it to the point of near-nonsense, how would you write a type which says `append "foo" "bar"` will always result in "foobar", and never "barfoo" or "fboaor"? Or that a theoretical celsiusToFahrenheit always works correctly and implements the correct calculation? If you can't do that, how can you do it for more complex data transforms?

A simpler example is that of lists and the head operation. In most languages, if you try to take the head of an empty list you get a runtime exception. In a language with dependent types you are able to express the length of the list in its type and thus it becomes a type error (caught at compile time) to take the head of an empty list.

Isn't that literally just implementing the program, though? The point of tests is that they're simple enough that you can't really fuck up, and they describe the specification, not the implementation.

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation?

The formal proof is the implementation. It is the code you run in production. The proposition is your types. Instead of writing tests, you write types. It's the exact same process you would use with "red-green-refactor" TDD except it's the compiler checking your implementation instead of the test suite. The advantage of doing it with types is that the compiler can actually infer significant parts of the implementation for you! Types also happen to be a lot more water-tight than tests due to the way you specify a type for a top-level function and everything inside of the body can generally be inferred.

If you're interested, here is a series of lectures demoing dependently-typed programming in Agda by Conor McBride:

https://www.youtube.com/playlist?list=PL_shDsyy0xhKhsBUaVXTJ...

The point of tests is that they're supposed to be simple enough that it should be near-impossible for them to contain bugs - they're incomplete, sure, but what they're testing should always be correct - whereas it seems that it would be easy for a proof to prove something subtly different from the spec without anybody being able to tell. If we could write complex programs to spec without error, we wouldn't have tests in the first place.

As for your assert example, how do you know append will work as you expect for all possible strings (including null characters or weird unicode edge cases)? With a proof you will know.

But I could just as easily accidentally write a proof which proves something else, couldn't I? This is complex code expressing complex ideas - a type system would certainly help, but it can't tell me that I'm proving the wrong thing.

Then your proof would be rejected by the compiler. Remember, the types specify your proposition: i.e. what you are intending to prove. The actual proof itself is the function you implement for that type.

As for whether you're proving the right thing or the wrong thing, a type system is no less helpful than a test suite. The advantage of a type system is that it checks whether your types are consistent within the entire program rather than in merely the specific test you're running.

Only for some types of mistake, surely. If that was always the case, we'd have a compiler that could read minds.

> As for whether you're proving the right thing or the wrong thing, a type system is no less helpful than a test suite.

Really? I can write down in my test suite, "assert (add 1 1) == 2". Anyone can come along and look at that and make sure it matches the spec. We can add additional tests for various bounds, and possibly use a quickcheck-like tool in addition, and for 99.99% of use cases be happy and confident that we're at least writing the right thing.

What's the type for that and does it actually have any resemblance to "the add function adds two numbers together", or do I have to read a couple of papers and have a background in university-level math to convince myself that the proof actually does what it says?

If you're modifying behavior, you will need to update the tests that break because of that, whether you write tests before or after.

This is a classic problem of externalities. You can only quantifiably judge what you are quantifiably measuring.

In this statement, you are only measuring the file couplings. I hope it's obvious that there are many other factors at play.

For example, let's look at a "typical" development iteration for a feature.

---

With TDD:

1. you write the automated test

2. run the test

3. if the test passes goto 6

4. edit the software

5. goto 2

6. finish

---

With manual testing:

1. edit the software

2. manually test the software

3. if the software does not do what you need it to do, goto 1

4. finish

TDD gives you a quick feedback loop, since the verification step is automated, at the cost of up front time spent on writing the test.

There's also automated regression testing, which is useful to prevent regressions when you change the software system.

---

When the software becomes complex:

* regression tests offer a quick feedback loop that scales almost linearly

* manual tests have a slower feedback loop and are often given to the QA staff, which involves communication overhead, scheduling, meetings, etc.

The solution there was for future languages to combine the two. Maybe we'll see a future language combine unit tests and source into the same file.

Heh, maybe such a language would refuse to compile if public functions did not have an associated test.

Sounds like my worst nightmare.