我使用区间算术进行可靠计算。现在,以良好的区间算术实现编码的过程可能需要大约八倍于没有区间算术执行的相同过程(如果运行时间的最大份额由浮点计算占据)。有时有人问我为什么不手动进行舍入误差分析。对我来说,这看起来不是一个好的选择:它相当于以牺牲人力来节省计算机时间,并为人为错误创造了更多机会。
现在,对我来说有意义的是在计算机的帮助下有一个用于限制舍入误差的系统。期望计算机在相当复杂的程序中分析总错误可能是不现实的,但是人和计算机可能能够比单独工作的人更快、更可靠地完成工作,并生成正确的证书以启动. 参照。在计算机辅助下如何更容易地生成正式证明。
(特别是:我会对如何在严格证明的上下文中使用例如威尔金森意义上的错误分析感兴趣。我可以看到如何通过计算机辅助系统来实现它正式证明的产生。在实践中是否做过这样的事情?)
注意:也许它显示了,但是——我是一个纯粹的数学家;如果我说的话似乎有点幼稚,请随时告诉我。