From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: =?utf-8?Q?=C3=93scar_Fuentes?= Newsgroups: gmane.emacs.help Subject: Re: if vs. when vs. and: style question Date: Mon, 30 Mar 2015 17:31:02 +0200 Message-ID: <87r3s6biyx.fsf@wanadoo.es> 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 X-Trace: ger.gmane.org 1427729538 21475 80.91.229.3 (30 Mar 2015 15:32:18 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 30 Mar 2015 15:32:18 +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 17:32:11 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 1Ycbfc-0004Kz-PB for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 17:32:08 +0200 Original-Received: from localhost ([::1]:34639 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Ycbfc-0007N1-66 for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 11:32:08 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:49780) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcbfQ-0007LB-9h for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 11:31:57 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1YcbfJ-0003R1-8I for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 11:31:56 -0400 Original-Received: from plane.gmane.org ([80.91.229.3]:54654) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcbfJ-0003Qm-1E for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 11:31:49 -0400 Original-Received: from list by plane.gmane.org with local (Exim 4.69) (envelope-from ) id 1YcbfA-0003xR-FP for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 17:31:40 +0200 Original-Received: from 171.red-80-26-206.adsl.dynamic.ccgg.telefonica.net ([80.26.206.171]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Mar 2015 17:31:40 +0200 Original-Received: from ofv by 171.red-80-26-206.adsl.dynamic.ccgg.telefonica.net with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Mar 2015 17:31:40 +0200 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 19 Original-X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: 171.red-80-26-206.adsl.dynamic.ccgg.telefonica.net User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.50 (gnu/linux) Cancel-Lock: sha1:iCN+15rUnu/hJ2j3bnzIDLQIKUg= X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 80.91.229.3 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:103453 Archived-At: 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). 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.