From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Emanuel Berg Newsgroups: gmane.emacs.help Subject: Re: CVE-2017-14482 - Red Hat Customer Portal Date: Mon, 25 Sep 2017 01:06:19 +0200 Message-ID: <867ewnae8k.fsf@zoho.com> 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> 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 1506294428 23694 195.159.176.226 (24 Sep 2017 23:07:08 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Sun, 24 Sep 2017 23:07:08 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.4 (gnu/linux) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Mon Sep 25 01:07:03 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 1dwFzJ-0005mb-L9 for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 01:07:01 +0200 Original-Received: from localhost ([::1]:39779 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwFzQ-00030u-QC for geh-help-gnu-emacs@m.gmane.org; Sun, 24 Sep 2017 19:07:08 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33482) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwFyu-00030e-F2 for help-gnu-emacs@gnu.org; Sun, 24 Sep 2017 19:06:37 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dwFyr-0003r7-A1 for help-gnu-emacs@gnu.org; Sun, 24 Sep 2017 19:06:36 -0400 Original-Received: from [195.159.176.226] (port=51622 helo=blaine.gmane.org) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dwFyr-0003qP-1y for help-gnu-emacs@gnu.org; Sun, 24 Sep 2017 19:06:33 -0400 Original-Received: from list by blaine.gmane.org with local (Exim 4.84_2) (envelope-from ) id 1dwFye-0003K4-Fx for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 01:06:20 +0200 X-Injected-Via-Gmane: http://gmane.org/ Mail-Followup-To: help-gnu-emacs@gnu.org Original-Lines: 50 Original-X-Complaints-To: usenet@blaine.gmane.org Mail-Copies-To: never Cancel-Lock: sha1:vHXBa5eLQyuZjoqylPuvMPsz/W0= 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:114393 Archived-At: Óscar Fuentes wrote: > It seems that you think that formal > verification says that the software is > correct. That's in theory. Practice is > different, as usual. > > Instead of writing a lengthy explanation > about why formal verification can't be > a guarantee about the correctness of a piece > of sotware, I'll simply reference a study > about failures on verified systems: Hold - perhaps the verification has to be verified as well? C'mon now, this is just another Computer Science hangup. Just like functional programming, or testing for that matter - which also is an academic pursuit, by the way! [1] - but as always, there is no silver bullet solution. If I'd send the space fleet to the oldest galaxies of the universe, I'd like all methods anyone could think of to make as sure as possible the software is correct. I'd start with very skilled and motivated programmers, proceed with sound programming practices, then code review, and then excessive testing. I suppose formal verification would be a distant fourth. [1] @book{ammann, author = {Paul Ammann and Jeff Offut}, title = {Introduction to Software Testing}, publisher = {Cambridge University Press}, year = 2008, ISBN = {978-0-521-88038-1}, edition = {6th edition} } -- underground experts united http://user.it.uu.se/~embe8573