それは証明系であって、汎用プログラミング言語じゃない。
コーディングしているのは証明。