Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.
Spark utilise aussi les SMT Z3 et CVC4 écrits tout deux en C++.
Par contre, j'avoue que je n'y connais rien et que je ne fais qu'utiliser, mon niveau de math étant bien en-deça du pré-requis ;)
[^] # Re: Solution à base de types variants en ADA
Posté par Blackknight (site web personnel, Mastodon) . En réponse à la dépêche Sortie de GHC 8.0.2 et une petite histoire de typage statique. Évalué à 2.
Spark utilise aussi les SMT Z3 et CVC4 écrits tout deux en C++.
Par contre, j'avoue que je n'y connais rien et que je ne fais qu'utiliser, mon niveau de math étant bien en-deça du pré-requis ;)