If you talk about evidence written on paper, the customs are essentially the same as in other languages: unofficial reasoning based on a reasonable (but not formalized) model of the semantics of the program. To handle your case, I would write two functions size and height and prove by inductive reasoning on the tree that size h <= pow 2 (height h + 1) - 1 , using the assumption of induction on two subtrees - I can make this explanation more detailed but I prefer to let you do it yourself if you want.
If you want more formal evidence, there are several approaches.
Hoare-based proof methods have been adapted to functional programming languages. See, for example, the work of Régis-Gianas and Pottier for 2008, Hoare Logic for Functional Programs by Default. They provide a formal basis for what can be used, still in written evidence, to give a stricter (because-to-metal) evidence of your claim. It can also be used in software, but I'm not sure that this approach is fully developed.
Another natural approach would be to write your program directly in the Coq helper, whose programming language is basically a purely functional subset of OCaml and use its features for proof. This is not quite the same as writing in OCaml, but pretty close; then you can either mirror the implementation in OCaml directly, or use the Coq extraction tool to get honest OCaml code that has been “compiled” from the Coq program. This approach was used to formalize the implementation of balanced binary trees present in the OCaml standard library, and the two implementations (OCaml one and Coq one) are synchronized enough that you can pass the results to confirm the correct changes in OCaml.
In the same vein, attempts are being made to develop languages for certified programming, which may be more convenient in some areas than the usual theoretical method, such as Coq. Why3 is such a "software verification platform": it defines programming languages (not very far from OCaml) and a specification language on top of It. You can formulate statements about your program and test them using various methods, such as general proof helpers (like Coq) or more automated theoretical proxies (SMT solvers). Why3 seeks to support verification of implementations of the classical imperative style algorithm, but also supports functional programming style, so for experiments with certified programming it may be an interesting choice if you do not want to switch to the full code (for example, if you're not interested in ensuring that your algorithms are complete which may be inconvenient in Coq).
Finally, the work was done according to the following method: read your OCaml program and automatically create a “Coq description” from it, with which you can familiarize yourself with the guarantee that what you think is correct is also contained in OCaml. This was the main result of the Arthur Charluro 2010 Ph.D. thesis , where the description of "Coq" is based on the method of "Characterization fomrulae". He was able to prove the correct ML implementations for complex algorithms such as Union-Find or examples from Chris Okasaki, the excellent book "Purely Functional Data Structures".
(I often mention the Coq proof helper, other tools like Isabelle and Agda are equally suitable, but Coq is closer in syntax to the OCaml language, so this is probably a good choice if you want to reimplement ML programs to validate them formally correctly. )