Test-First Development
The usual order of development is to implement first and then write the tests. The reverse is called test-first development. Since we are writing the tests against the contract, we can write them before any implementation exists.
What does writing the test first give you?
The test is an executable specification. To write it, you must decide what the method should do: what inputs it takes, what it returns, and what it promises. You decide all of that before you write any code. This helps you better understand the contract before you implement it.
It is hard to demonstrate the value of test-first with a simple abstraction like List. The value becomes clearer when you are implementing more complex abstractions, where the contract is more complicated and the implementation is more subtle.
The test-first approach is a popular technique in industry. Although, a variant of it, called test-driven development (TDD), is more common. TDD is test-first, but it works in a smaller loop. Instead of writing a whole suite of tests up front, you write one test, then implement just enough code to make it pass, then write the next test, and so on. You are developing the code and its tests together.
Passing tests are evidence of correctness, not proof. The tests only check the inputs you thought to write down. They do not check every possible input. Proving that the code is correct for every possible input is called formal verification, and it is a different and much harder job. Tests are what we use day to day. They give us enough evidence to build on the code and to change it.