Why not include little proofs in the code when you can?
Several programming languages and libraries support Design-by-Contract (https://en.wikipedia.org/wiki/Design_by_contract) which lets you specify preconditions, postconditions, and invariants directly in your code.
Those predicates can be checked in various ways (depending on how deeply Design-by-Contract is supported) to help you know that your code is working correctly.
Ada supports Design-by-Contract as part of the language: https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
SPARK extends Ada Design-by-Contract into full proofs: https://learn.adacore.com/courses/intro-to-spark/index.html
Rust has the Contracts crate: https://docs.rs/contracts/latest/contracts/
Other programming languages have various levels of support or libraries for Design-by-Contract: https://en.wikipedia.org/wiki/Design_by_contract#Language_su...
Even standard assertions work as a version of this
Standard assertions certainly are better than keeping the little proofs only in your head.
Many Design-by-Contract implementations are nicer than standard assertions because they help to express intent better and easily refer to the 'old' value of a parameter to verify desired results.