unofficial mirror of help-gnu-emacs@gnu.org
 help / color / mirror / Atom feed
From: Emanuel Berg <moasen@zoho.com>
To: help-gnu-emacs@gnu.org
Subject: Re: CVE-2017-14482 - Red Hat Customer Portal
Date: Mon, 25 Sep 2017 01:06:19 +0200	[thread overview]
Message-ID: <867ewnae8k.fsf@zoho.com> (raw)
In-Reply-To: 87vak8rwcx.fsf@qcore

Ó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




  parent reply	other threads:[~2017-09-24 23:06 UTC|newest]

Thread overview: 68+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-09-21 21:51 CVE-2017-14482 - Red Hat Customer Portal ken
2017-09-21 22:03 ` Kaushal Modi
2017-09-21 23:07   ` ken
2017-09-22  7:37     ` Alberto Luaces
2017-09-22  7:48       ` Emanuel Berg
2017-09-22 20:12         ` Mario Castelán Castro
2017-09-22 22:14           ` Emanuel Berg
2017-09-24  2:08             ` Mario Castelán Castro
     [not found]             ` <mailman.1063.1506218941.14750.help-gnu-emacs@gnu.org>
2017-09-24  6:47               ` Emanuel Berg
2017-09-24 13:38                 ` Mario Castelán Castro
2017-09-24 14:42                   ` Óscar Fuentes
2017-09-24 14:54                     ` tomas
2017-09-26 18:57                       ` Narendra Joshi
2017-09-24 23:06                     ` Emanuel Berg [this message]
2017-09-25 21:23                       ` Mario Castelán Castro
2017-09-25 21:49                         ` Emanuel Berg
2017-09-26  1:43                           ` Mario Castelán Castro
2017-09-26  2:17                             ` Emanuel Berg
2017-09-25 21:11                     ` Mario Castelán Castro
2017-09-25 23:58                       ` Óscar Fuentes
2017-09-26 14:46                         ` Mario Castelán Castro
2017-09-26 23:31                           ` Óscar Fuentes
2017-09-29 20:21                             ` Mario Castelán Castro
2017-09-29 12:43                           ` Eli Zaretskii
2017-09-29 14:59                             ` dekkzz78
2017-09-29 16:51                               ` Óscar Fuentes
2017-09-29 17:20                                 ` Emanuel Berg
2017-09-29 18:27                                   ` Óscar Fuentes
2017-09-29 19:45                                     ` Emanuel Berg
2017-09-29 20:06                                       ` Óscar Fuentes
2017-09-29 23:24                                         ` Emanuel Berg
2017-09-29 18:03                               ` Eli Zaretskii
2017-09-24 23:07                   ` Emanuel Berg
2017-09-23 10:05           ` Charles A. Roelli
2017-09-23 12:53             ` Óscar Fuentes
2017-09-23 13:12               ` Eli Zaretskii
2017-09-23 17:18                 ` Glenn Morris
2017-09-23 17:34                   ` Eli Zaretskii
2017-09-23 20:50                     ` Yuri Khan
2017-09-24  2:53                       ` Eli Zaretskii
2017-09-24  7:13                         ` Philipp Stephani
2017-09-24 18:29                           ` Robert Thorpe
2017-09-29  8:17                             ` Eli Zaretskii
2017-09-29 20:28                             ` Stefan Monnier
2017-09-29 23:28                               ` Emanuel Berg
2017-10-03  0:52                                 ` Stefan Monnier
2017-10-03  1:04                                   ` Emanuel Berg
2017-09-29  7:11                           ` Eli Zaretskii
     [not found]                         ` <mailman.1068.1506237251.14750.help-gnu-emacs@gnu.org>
2017-09-24  7:48                           ` Emanuel Berg
2017-09-25 21:26                         ` Glenn Morris
2017-09-25 22:02                           ` Emanuel Berg
2017-09-25 22:08                           ` Ludwig, Mark
2017-09-26  5:50                             ` Emanuel Berg
2017-09-26 13:40                               ` Ludwig, Mark
2017-09-26 17:46                             ` Philipp Stephani
2017-09-26 19:00                               ` Ludwig, Mark
2017-09-29 13:23                               ` Eli Zaretskii
2017-09-29  9:48                           ` Eli Zaretskii
2017-09-26 18:44                   ` Narendra Joshi
2017-09-26 18:51                     ` Philipp Stephani
     [not found]           ` <mailman.988.1506161159.14750.help-gnu-emacs@gnu.org>
2017-09-24  6:31             ` Emanuel Berg
2017-09-22 16:40       ` ken
2017-09-22 19:07         ` Emanuel Berg
2017-09-23 20:27     ` Bob Proulx
     [not found]     ` <mailman.1053.1506198486.14750.help-gnu-emacs@gnu.org>
2017-09-24  6:38       ` Emanuel Berg
2017-09-24 17:17         ` Maxim Cournoyer
2017-09-24 22:38           ` Emanuel Berg
  -- strict thread matches above, loose matches on Subject: below --
2017-09-27 10:51 Richard Melville

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

  List information: https://www.gnu.org/software/emacs/

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=867ewnae8k.fsf@zoho.com \
    --to=moasen@zoho.com \
    --cc=help-gnu-emacs@gnu.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).