> Do you have any reason to believe that all the rest of the verification theory is completely impractical when every piece that was packaged in a usable context became a hit?

While I am by no means have enough knowledge to claim such, but let’s just add that ordinary types are a so-called “trivial property”. Many, actually interesting properties can’t be proved as per Rice’s theorem in every case.