I like this quote in "From Zero to QED":
"The honest truth is that most people do not need dependent type theory or formal verification for their day jobs. But necessity is a boring criterion for what to learn. People study ancient languages, play chess, learn to cook elaborate dishes, prove that there are infinitely many primes. The question is not whether you need something but whether it interests you."
