This is my personal site. I intend to share my ideas here. I am a physicist and currently work as a C++ developer. My interest include formal proofs and their application to computer algebra systems and program source code verification.