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.
