There is a place for informal, prose specs, and I can easily agree that more people are nowadays describing their programs in English.

The context here is formal specs though - adequately and precisely capturing the intended meaning (semantics) in a way that lends itself to formal verification.

Interactive theorem proving is interactive because proof search is intractable; a human articulates the property they want to prove and then performs the "search". Apart from the difficulties of getting to that proof, it can also happen that all goes through and you realize that the property is not exactly what you wanted.