I'm not sure what point you're trying to make. You can certainly express those statements in both FP and imperative languages, and you can prove the equivalences you mention in FP languages like Agda, Coq, and F*.
The type level of dependently typed languages or other languages that allow directly expressing relations (including Java's JML) can do that. That's little to do with pure FP.
In some sense it does though. Type Theories (and their associated pure FP languages) often have the exact same algebraic structure as different classes of logic. To my understanding, JML uses Hoare Logic, which is a great tool for proving correctness of imperative languages, but is not quite as expressive. For example, Hoare Logic cant really deal with Higher-Order things. That's not to say Coq/Agda are perfect though. They do struggle with more "extensional" properties, such as function extensionality.
> For example, Hoare Logic cant really deal with Higher-Order things.
1. It can. 2. It doesn't matter so much, as there are no higher order "things" but rather higher-order ways to describe things. For example, in mathematics higher-order systems can be described as either higher-order ODEs or equivalent first-order ODEs. In other words, "order" is a feature of the signifier, not the signified. For example, things that would be higher-order in Agda are first-order in TLA+ (and you don't need to go that far: formal set theories are usually first-order, yet you need higher-order typed logics to describe the same things).
> They do struggle with more "extensional" properties, such as function extensionality.
Well, that's because they're constructive. There are type-theory-based proof assistants that more easily support classical mathematics, like Lean.
First, while you can express those statements in programming languages, they will either be expressed differently in order to have the same meaning or, if expressed in a similar way, have a different meaning (even ignoring that many such statements are not computable at all). This merely shows that math is not an FP language.
Second, you can prove those equivalences in any language that allows you to directly express relations, be it the type-level language of Agda, Coq or F*, or the contract language of an imperative language -- this is nothing to do with FP, but with a language that can express relations.
