Hit the nail on the head. The major problem with NN is that they are completely unexplainable black boxes. The algorithm spits out a piece of code (or recommend

Hit the nail on the head. The major problem with NN is that they are completely unexplainable black boxes. The algorithm spits out a piece of code (or recommends clickbait videos, or bans you from a website, or denies you credit) based on a mishmash of assorted examples and a few million/billion parameters, but can neither explain why it picked it, nor verify that it is correct. Formal methods and theorem proving on the other hand, place a strong emphasis on proof production and verification.