众所周知，数学以系统的混乱、诸多悖论、难学著称。我看过许多证明，发现一个问题：数学的符号和变量等完全可以用编程中的系统，这样学数学就和重新学一门编程语言一样了。比如说一下是我尝试用C++写的一段数学证明（不是很完善，轻喷）：

#include<peano>//皮亚诺公理（包含了逻辑系统<boolean>，已省略）
using namespace peano;
//S1:isNumber(0)
//S2:isNumber(numberNext(n))==isNumber(n)
//S3:numberNext(n)!=0
//S4:numberNext(n)!=numberNext(m) && (n!=m)
//S5:isFuncTrue(f){return f(0) && (f(n)==true);}
//在<peano>中，公理S1~S5均成立
//上述公理中：
//isNumber定义为接受任意类型的变量，返回是否为变量自然数
//numberNext定义为接受一个自然数，返回自然数的后继
//以上两个函数必须满足S1~S4
//n,m定义为isNumber(n)==true && isNumber(m)==true为真的数。以后描述isNumber(n)为true的变量类型是number类型
//S5没有找到一个比较好的表达方式。应该表述为f(0)为true且f(n)为true，其中n是number类型的
//自然数的判断略，没有找到比较好的定义方式
number add(number n,number m,number s=0){//加法，等价于n+m。新增一个变量s是技术原因。
	if(boolean(s==0)){
		return add(0,m,n);
	}
	if(n==m){
		return s;
	}
	return add(numberNext(n),m,numberNext(s));
}
boolean proposition(number n){//假设命题对n成立，求证命题对numberNext(n)是否成立
	//当前命题等价于：n+1==n'
	return add(numberNext(n),numberNext(0))==numberNext(n);//always true
}
int main(){
	if(isFuncTrue(proposition)){
		return 0;//succesful
	} else{
		return 1;//faild
	}
}

诸如此类，像这样把数学重新描述为一种编程语言并且所有（或某个体系下）数学的命题、公理、结论都能用这种语言写出来。这种编程语言可能存在吗？

（并且如果有的话建议oiwiki用这种语言写一遍，我看懂数学的证明没比看懂编程代码容易）