Missing mechanism to check that assumptions are correct

[RCoeurjoly]

As far as I can tell, there is no mechanism for checking that the assumptions of a certain function hold.

Quoting from https://www.tweag.io/blog/2023-06-22-lh-assumption-imports/#idea-separating-annotations-and-definitions:

Proving that map yields some property of interest does often require its definition.

I am curious about the often part of that quote.

Let's say that the definition of a function is not available, but I have its assumptions.
Is there a way to prove that the function fulfils all its assumptions?

Missing a formal proof, it would also be valuable from my point of view to do runtime checks of those assumptions.

[facundominguez]

Is there a way to prove that the function fulfils all its assumptions?

Assumptions are not meant to be proved, they are assumed without proof. But maybe you mean that you would like to promote an assumption to a lemma and then prove it.

It could be helpful to have an example of an assumption that you would like to promote. Without the definition of the function, we surely would have to rely on yet other assumptions for the proof.

Missing a formal proof, it would also be valuable from my point of view to do runtime checks of those assumptions.

This could mean, for instance, writing tests to check the assumptions. It is possible, but does LH need to be involved when writing these tests?