情報科学の研究者とかならともかく、一般のプログラマがプログラムが正しいことを
数学的に証明とかしないでしょ。