Type checking, compile-time errors won't check if the program you wrote is correct, only that it's internally consistent. That is an entirely different thing than checking for correctness.
You do need a layer of tests that actually try to prove that given some input your program actually does what it's supposed to do. That is hard to automate.
Joe Armstrong(of the Erlang fame), talks about this a bit here: https://youtu.be/TTM_b7EJg5E?t=778
I've pointed to a specific timestamp, but there might be more details somewhere else in that talk.
That's untrue. There are type-systems and type-checkers which can check for correctness, as specified by a mathematical formula. This is proof assistants such as Coq[1] work. For example, take a look at fiat-crypto [2], a project that generates code that is correct by mathematical proof, and is now deployed in Chrome. Another famous example is the CompCert [3] compiler, a C compiler along with a correctness proof that the compiler generates assembly which correctly simulates the C semantics.
These are based on powerful types as "dependent types" which can encode mathematics and programs in the same programming language, and allow the mathematics to "talk about" the program. The mathematical underpinning is the Curry-Howard-Lambek correspondence.
[1] https://coq.inria.fr/ [2] https://github.com/mit-plv/fiat-crypto [3] https://compcert.org/ [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
> Wouldn't it be cool if we could have code that would test itself?
> Yeah, if only there were some kind of automated way to encapsulate the requirements of classes and methods that could ensure that they behaved within some known boundaries...?
We've had automated unit tests for quite some time, but they are more often called compiler checks. Want your "automated unit tests" to be more comprehensive? Improve your type system and your compiler!
With all that said, I do not want to be dismissive of peoples' projects. This is fun and neat.