From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: "Pascal J. Bourguignon" Newsgroups: gmane.emacs.help Subject: Re: if vs. when vs. and: style question Date: Mon, 30 Mar 2015 19:15:51 +0200 Organization: Informatimago Message-ID: <87sicmwgmw.fsf@kuiper.lan.informatimago.com> References: <87lhilx0cf.fsf@debian.uxu> <87twx9360u.fsf@kuiper.lan.informatimago.com> <0d1d19ab-06e9-462d-8867-9a49b1e232d3@googlegroups.com> <87pp7x2jav.fsf@kuiper.lan.informatimago.com> <87d23s4nt4.fsf@debian.uxu> <7e8ddf8f-163a-4d16-9ce2-25b0cb3f35aa@googlegroups.com> <87sicny7zm.fsf@kuiper.lan.informatimago.com> <874mp3clqi.fsf@wanadoo.es> <20150330094432.GA30418@tuxteam.de> <87a8yuy6wn.fsf@kuiper.lan.informatimago.com> <871tk68qa4.fsf@wmi.amu.edu.pl> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1427736355 19158 80.91.229.3 (30 Mar 2015 17:25:55 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 30 Mar 2015 17:25:55 +0000 (UTC) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Mon Mar 30 19:25:40 2015 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1YcdRC-0007Wj-0V for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 19:25:22 +0200 Original-Received: from localhost ([::1]:35336 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcdRB-0000sj-8E for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 13:25:21 -0400 Original-Path: usenet.stanford.edu!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail Original-Newsgroups: gnu.emacs.help Original-Lines: 49 Original-X-Trace: individual.net lBCzU9NCTJXgJgfWQLLqGglNqqPY0hsxgVlsZ1jV+3WjSOWDqo Cancel-Lock: sha1:NWQyMDA3OTljY2IxYmUxMmNhNWY0M2VjYzQwMTY3M2JjZmRmMTcwNQ== sha1:eepHFV6HEp2rV+9MSUE5yCGEgng= Face: iVBORw0KGgoAAAANSUhEUgAAADAAAAAwAQMAAABtzGvEAAAABlBMVEUAAAD///+l2Z/dAAAA oElEQVR4nK3OsRHCMAwF0O8YQufUNIQRGIAja9CxSA55AxZgFO4coMgYrEDDQZWPIlNAjwq9 033pbOBPtbXuB6PKNBn5gZkhGa86Z4x2wE67O+06WxGD/HCOGR0deY3f9Ijwwt7rNGNf6Oac l/GuZTF1wFGKiYYHKSFAkjIo1b6sCYS1sVmFhhhahKQssRjRT90ITWUk6vvK3RsPGs+M1RuR mV+hO/VvFAAAAABJRU5ErkJggg== X-Accept-Language: fr, es, en User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) Original-Xref: usenet.stanford.edu gnu.emacs.help:211176 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.help:103458 Archived-At: Óscar Fuentes writes: > Marcin Borkowski writes: > >>> Along the same lines, I don't know many programmers whose code is never >>> passed to a compiler/interpreter but is instead only read by other >>> human beings. >> >> BTW: I think you nailed a serious problem with contemporary mathematics: >> that machine checking proofs isn't a routine part of the publishing >> process. The number of erroneous papers in math journals is >> horrifying. Substantial portion of my depatment's seminar is devoted to >> discussing errors in papers. Once a colleague found a relatively simple >> /counterexample/ to a theorem which was a cornerstone of a whole theory >> (and a basis for several dozen other papers). Perhaps it's not pertinent in a specific case, but I'd see it as much as a question of what axioms or inference rules would be needed to prevent those counter examples, and thus validate the theory developed so far, as the need to revise the validity of that theorem and its supposed consequences. > Yeah, that remembers me of Vladimir Voevodsky's story about why he > always has a Coq session running nearby. > > OTOH I'm afraid that proof assistants can be a hindrance for creative > work. Perhaps they should work both way: - deduce consequences from axioms (or check deductions), and - find axioms and deduction rules that would allow a given "chain of reasoning" to be a theorem. If you only knew Euclidian geometry and imagined a triangle whose sum of angles was 200 degree, you'd want a formal tool to help you infer spherical geometry's axioms. -- __Pascal Bourguignon__ http://www.informatimago.com/ “The factory of the future will have only two employees, a man and a dog. The man will be there to feed the dog. The dog will be there to keep the man from touching the equipment.” -- Carl Bass CEO Autodesk