From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: =?utf-8?Q?=C3=93scar_Fuentes?= Newsgroups: gmane.emacs.help Subject: Re: CVE-2017-14482 - Red Hat Customer Portal Date: Wed, 27 Sep 2017 01:31:57 +0200 Message-ID: <87d16drq8i.fsf@qcore> References: <2e991bb7-c570-49ce-be94-3654945bb4b5@mousecar.com> <87d16jxjz6.fsf@eps142.cdf.udc.es> <861smzcgx3.fsf@zoho.com> <1b3bec6e-d4d5-37a7-ba54-49bd2d8281bd@yandex.com> <86k20qbcu9.fsf@zoho.com> <86o9q0a8zc.fsf@zoho.com> <87vak8rwcx.fsf@qcore> <87mv5is54g.fsf@qcore> <4d048ea0-5c54-f5ba-c903-78614480ac76@yandex.com> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: blaine.gmane.org 1506468769 2076 195.159.176.226 (26 Sep 2017 23:32:49 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 26 Sep 2017 23:32:49 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.0.50 (gnu/linux) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Wed Sep 27 01:32:44 2017 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dwzLG-0008SM-0b for geh-help-gnu-emacs@m.gmane.org; Wed, 27 Sep 2017 01:32:42 +0200 Original-Received: from localhost ([::1]:51462 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwzLN-0008Lw-CV for geh-help-gnu-emacs@m.gmane.org; Tue, 26 Sep 2017 19:32:49 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:55509) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwzKv-0008Lf-IJ for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 19:32:23 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dwzKq-0000cF-LU for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 19:32:21 -0400 Original-Received: from [195.159.176.226] (port=53056 helo=blaine.gmane.org) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dwzKq-0000bn-E4 for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 19:32:16 -0400 Original-Received: from list by blaine.gmane.org with local (Exim 4.84_2) (envelope-from ) id 1dwzKc-00061V-Ci for help-gnu-emacs@gnu.org; Wed, 27 Sep 2017 01:32:02 +0200 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 130 Original-X-Complaints-To: usenet@blaine.gmane.org Cancel-Lock: sha1:Q67+z9IC68yDtSrEBx/BaRyD4Ck= X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 195.159.176.226 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.21 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" Xref: news.gmane.org gmane.emacs.help:114432 Archived-At: Mario Castelán Castro writes: > On 25/09/17 18:58, Óscar Fuentes wrote: >> Mario Castelán Castro writes: >>> This depends on what exactly is meant by “correct”. >> >> "correct" means that the client (the people who required the software) >> says that the program fulfills his requirements. Sometimes you need to >> wait an infinite amount of time for obtaining client's approbation :-) > > The same answer applies: If a client either provides himself or accepts > a formula in formal logic as a description of his requirements, then > yes, we can prove that a program is correct according to this concept. > > If the client can not provide an *absolutely accurate* description (this > is necessarily a specification in formal logic) of what his requirements > are, then we can not assure the client that the program meets his > requirements. This is not a fault of the programmer, but of the client > for being vague about what his requirements are. > >>> If by “correctness” it is meant a formula in *formal logic*, then yes, >>> we can prove that the program behaves correctly. >> >> Ever heard of a chap named Kurt Gödel? Or his cousin Alan Turing? :-) > > What you are doing here is intellectual fraud. You are conveying the > impression that there is an obstacle that prevents formal verification, > yet you did not even _mention_ what this obstacle is. > > Given that you mentioned Gödel, I guess (I can merely *guess* your > intent because you did not explain it; this is your fault, not mine) > that you believe that either the Gödel-Rosser incompleteness > theorem[Mend, p. 210] or one of the many variations is an obstacle for > formal verification. This is incorrect. What these theorems state is > that in any formal system that meets certain prerequisites, there is an > assertion P such that neither P nor ¬P are a theorem of the formal > system. Also, it seems that you are confusing algorithmic undecidable > problems (like the halting problem) with formally undecidability > propositions (like the axiom of choice within ZF). > > In practice, using well-established logic systems (e.g.: HOL and ZFC) > one does not _accidentally_ runs into formally undecidable statements. > Moreover, suppose that you are “sure” that a certain proposition P that > is undecidable in (say) HOL is “true”. What should you do? Since you are > sure that P is “true”, then you must have proved P it in _some_ formal > system (otherwise your claim has no logical basis) and you trust that > this formal system is consistent. You can then either embed your formal > system within HOL, or add the appropriate axioms (both options are a > routine procedure in most proof assistants), and then prove P within > your embedding in HOL or within your HOL+axioms system. > > Also, it is dubious whether it is a good idea to write a program whose > correctness depends on baroque axioms like large cardinals. This > commentary holds regardless of whether you are interested in formally > proving its correctness. > >> […] it >> is almost certain that there are "correct" informal specifications that >> do not admit a verifiable formal specification. > > This is yet more intellectual fraud (an unjustified claim). > > ***** > I have spent already enough time addressing your misconceptions. If you > reply to this message with even more misconceptions, I will not reply > because I am unwilling to spend even more time explaining what you > should already know. It is *YOUR* task to make sure you know what you > are talking about (and you have failed so far), not mine!. > Well, as a humble software developer who is happy whenever I get things done "well enough", let me ask a few simple questions. You can simply respond with "yes" or "no", if you wish: * Is there a proof that demonstrates that every program admits a verifiable formal specification, or a method for knowing in advance which programs admit such specification? * Is there a proof that demonstrates that the verification will take a maximum amount of computing resources? (let's say polinomial on some metric of the program's code). * Are there reliable methods for estimating the amount of man/hours (give or take one order of magnitude) required for creating a verifiable formal specification from some informal specification language used in the industry? * Are there studies that, based on past practice, demonstrate that the formal approach is more economic than the traditional one, either along the development phase or along the complete life cycle of the software? >> […] We must provide what is requested from us, in >> terms of functionality, performance and cost […] > > Somebody has to take a decision between cheap software and reliable > software. Those are mutually exclusive. > > The predominating choice is cheap software. As evidence for this claim I > note the very high frequency of bug reports including security > vulnerabilities. Categorizing software as "cheap" or "reliable" misses the point entirely. Either the software is adequate or not. And the adequateness criteria varies wildly, but two things are always present: if your sofware is more expensive than the value it provides, it is inadequate; if your software takes too much time to develop, it is inadequate. I've seen too many academics that fail to understand those simple facts. > If you are interested in formal logic, either because of genuine > interest or just to criticize, I suggest [Mend] as a starting point. > > [Mend] E. Mendelson “Introduction to Mathematical Logic”, 6th edition > (2015). Many years ago I felt in love with mathematical logic and devoted many many (that's two manys) hours to its study. In the end I decided that was impractical and sterile and forgot almost everything. Since, automatic theorem provers got much better to the point of being usable for certain types of problems. Right now, I'm looking forward to implementing dependent types on my programming language. I have Coq and Idris around and played with it but so far I failed to see them as an improvement on my work. That means that it is exciting and feels promising, but I see no clear gain from using them. With age, I turned skeptic about new things. If formal methods is the silver bullet, the proponents are those who must provide evidence and so far it is missing, apart from some niche cases (and then the evidence is dubious, as shown on the paper that I mentioned on a previous message).