One of the important advantages of having a mathematical model for programming is that it’s possible to perform formal proofs of correctness of software. This might not seem so important when you’re writing consumer software, but there are areas of programming where the price of failure may be exorbitant, or where human life is at stake. But even when writing web applications for the health system, you may appreciate the thought that functions and algorithms from the Haskell standard library come with proofs of correctness.
Unit testing may catch some of the mismatches, but testing is almost always a probabilistic rather than a deterministic process. Testing is a poor substitute for proof. - Bartosz Milewski
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Z3 is a theorem prover from Microsoft Research
https://github.com/Z3Prover/z3
LEAN - LANGUAGE FOR THEOREM PROOF
https://lean-lang.org/documentation/