Comment by bsaul

in practice, what kind of proof are people building when building real world programs ?

Are people writing only top level assertion ( such as "this main function always terminate") and the checker points at all the gaps ?

Or does one has to write proofs for every single intermediate layer and functions ?

In wich case, do people then have access to prebuilt "proven functions" in a stdlib ? such as "NeverEmptyList" or "AlwaysGreaterThanXVariable" ?