I'm not claiming to not write tests. I am claiming that there's a class of tests that do not need to be written if a formal proof system is guaranteeing the res

I'm not claiming to not write tests. I am claiming that there's a class of tests that do not need to be written if a formal proof system is guaranteeing the results. I don't need to write a test to see that `Math.sin("banana")` behaves properly, because the type system can guarantee that this doesn't happen.