On Jul 26, 1:51 am, rjf <fate...@gmail.com> wrote: <SNIP> > I hope that Bill was hoping to stir up some dissenting opinions.
Yes, naturally. However, it looks to me that you have simply recorded the way things currently are. People will do whatever they feel like. That's true by definition. Regarding rigor, mathematics itself went through a phase where informal arguments were displaced with formal ones. Likewise, informal computer programs will eventually give way to formally verified ones, and this will naturally be embraced by mathematicians. You are right that this will not directly have an effect on Number Theory computations as they are currently done because people will continue to use computers as a tool to investigate conjectures and collect numerical evidence and so on. They care little about whether the program is correct. I'm also not talking about program proving in the sense that people usually mean it. I simply mean that compiler technology will give more confidence in implementations by virtue of the fact that they will check things currently left unchecked. This will obviously be picked up by serious mathematicians, namely the ones who are currently growing up with computers and who come to care about rigor, and will be made a formal part of doing mathematics with computers. I don't envision some centralised authority imposing conditions on published work. It will simply become part of mathematics de rigueur. Reearchers will not risk submitting papers that may be rejected on the grounds of inappropriate formal justification of their code for the standard of journal they are submitting to. When people begin justifying their programs in their papers, (which will of course also be electronic in the future), then the field will become more academically sound and eventually the problems it currently has will become a thing of the past. At the moment the field (if you can even call it that) has a serious image problem. People speak about working on computation in whispers as though it is sinful. This is possibly something you don't encounter as a computer scientist. Bill. -- To post to this group, send an email to sage-devel@googlegroups.com To unsubscribe from this group, send an email to sage-devel+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org
