[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: if vs. when vs. and: style question

From: Óscar Fuentes
Subject: Re: if vs. when vs. and: style question
Date: Mon, 30 Mar 2015 17:31:02 +0200
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.50 (gnu/linux)

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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]