> But you literally cannot possibly test that assertion for all x. Hence why he states it is formal verification for the "unwashed masses". The "washed" will u

> But you literally cannot possibly test that assertion for all x. Hence why he states it is formal verification for the "unwashed masses". The "washed" will use a language with a type system that is advanced enough to express a formal proof, but most people can't hack it, and thus use languages with incomplete type systems and use testing to try and fill in the gaps.