Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

If the code and the comments disagree, then both are probably wrong. -- Norm Schryer


devel / comp.lang.python / Re: Question(s)

SubjectAuthor
o Re: Question(s)Thomas Passin

1
Re: Question(s)

<mailman.45.1698196218.3828.python-list@python.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=24189&group=comp.lang.python#24189

  copy link   Newsgroups: comp.lang.python
Path: i2pn2.org!i2pn.org!news.swapon.de!fu-berlin.de!uni-berlin.de!not-for-mail
From: lis...@tompassin.net (Thomas Passin)
Newsgroups: comp.lang.python
Subject: Re: Question(s)
Date: Tue, 24 Oct 2023 21:10:13 -0400
Lines: 59
Message-ID: <mailman.45.1698196218.3828.python-list@python.org>
References: <CAPpdf58WXyJs+Rd_GnbS-6dW8bPNt5DsojnVN5_ep+ebNx36Pw@mail.gmail.com>
<58b56dbe-646c-4a94-8102-ac2cf6efe233@tompassin.net>
<CAPpdf5_WVe07YVm-dZVV1mpZSWB6v4Z0itRsfYxYVdt8bWt0Ng@mail.gmail.com>
<da70b32a-28a3-4a7d-a403-53906cade994@tompassin.net>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
X-Trace: news.uni-berlin.de /shqNQVY6u+OvGrdXtUOfgD2SK0h/5bi5iygcBbi12kA==
Cancel-Lock: sha1:JGaWFgOH0g3gOMPNZjHLAK6JcmQ= sha256:OtxFo0y4k7ZDa2WGlhybQBspsgLM3MgAPJZOCDykXZo=
Return-Path: <list1@tompassin.net>
X-Original-To: python-list@python.org
Delivered-To: python-list@mail.python.org
Authentication-Results: mail.python.org; dkim=pass
reason="2048-bit key; unprotected key"
header.d=tompassin.net header.i=@tompassin.net header.b=G6XKfMfi;
dkim-adsp=pass; dkim-atps=neutral
X-Spam-Status: OK 0.005
X-Spam-Evidence: '*H*': 0.99; '*S*': 0.00; 'absolute': 0.05;
'programming.': 0.05; '2023': 0.07; 'else.': 0.07; 'formal': 0.07;
'general,': 0.09; 'received:23.83.212': 0.09;
'received:elm.relay.mailchannels.net': 0.09; 'responses': 0.09;
'problem.': 0.15; 'that.': 0.15; 'arbitrary': 0.16; 'bugs': 0.16;
'bugs.': 0.16; 'computation.': 0.16; 'create,': 0.16; 'general.':
0.16; 'impossible': 0.16; 'mathematical': 0.16; 'means.': 0.16;
'o1bigtenor': 0.16; 'personally,': 0.16; 'received:10.0.0': 0.16;
'received:23.83.212.17': 0.16; 'received:64.90': 0.16;
'received:64.90.62': 0.16; 'received:64.90.62.162': 0.16;
'received:bird.elm.relay.mailchannels.net': 0.16;
'received:dreamhost.com': 0.16; 'sounds': 0.16; 'those?': 0.16;
'which,': 0.16; 'wrote:': 0.16; 'hardware': 0.19; 'pm,': 0.19;
'subject:Question': 0.19; 'tue,': 0.19; 'to:addr:python-list':
0.20; "i've": 0.22; 'basically': 0.22; 'code': 0.23; 'anything':
0.25; 'cannot': 0.25; 'programming': 0.25; 'done': 0.28;
'computer': 0.29; 'asked': 0.29; 'header:User-Agent:1': 0.30;
'program': 0.31; "doesn't": 0.32; 'mission': 0.32; 'python-list':
0.32; 'received:10.0': 0.32; 'received:mailchannels.net': 0.32;
'received:relay.mailchannels.net': 0.32; 'structure': 0.32; "i'm":
0.33; 'there': 0.33; 'mean': 0.34; 'header:In-Reply-To:1': 0.34;
'developed': 0.35; 'question.': 0.35; 'couple': 0.37; 'could':
0.38; 'read': 0.38; 'difficult': 0.40; 'learn': 0.40; 'something':
0.40; 'want': 0.40; 'team': 0.60; "there's": 0.61; 'here': 0.62;
'come': 0.62; 'subject': 0.63; 'true': 0.63; 'ever': 0.63; 'full':
0.64; 'subject:(': 0.64; 'your': 0.64; 'touch': 0.65; 'well':
0.65; 'less': 0.65; 'header:Received:6': 0.67; 'technical': 0.67;
'received:64': 0.67; 'within': 0.69; 'experience.': 0.70;
'interesting': 0.71; 'read,': 0.75; 'proven': 0.76; 'business':
0.77; 'out.': 0.80; 'ambitious': 0.84; 'certainty': 0.84;
'itself.': 0.84; 'moon': 0.84; 'errors,': 0.91; 'mistakes': 0.91
X-Sender-Id: dreamhost|x-authsender|tpassin@tompassin.net
ARC-Seal: i=1; s=arc-2022; d=mailchannels.net; t=1698196214; a=rsa-sha256;
cv=none;
b=y0rbopvDwwYyeiytb7KCFYxStZ+4a496XIwTtfFAD5PIrYWKYIqAfwcV6coGQHyJAPke+s
nI56CjgJAaZUA6W6VwkiMc347NzjXXE3nrBJfbwNTDhc9+LmvzuHjblwwjwZBgwKGkxFtk
DuXnRnrTAJ9LUo6vn1Aam8dg4rbS1sdrSipvLyYxSJXtd2te5gKir7rhBa8i0cH1snElib
A+w7rjn8ORdXTetDBmg/dZcBbZUpVNGMpk67T8Ixo/o+m6UpPtI9IXNgA1SV/9Jg7UHQO0
Ml9rCBUiP2vRXLm+l6a9tSGJct8D7JB//b3OV50sGTQ5xEcvOYBH7BejTyzsyQ==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed;
d=mailchannels.net; s=arc-2022; t=1698196214;
h=from:from:reply-to:subject:subject:date:date:message-id:message-id:
to:to:cc:mime-version:mime-version:content-type:content-type:
content-transfer-encoding:content-transfer-encoding:
in-reply-to:in-reply-to:references:references:dkim-signature;
bh=xFcYN+epc2DTu7JeNXgq5KBUkMRB/graWShiz/uw80c=;
b=vwwvVEIafF036Zvsi/OAzMI/RCQU1wm0DFpdGb9EWWHIhhkWujmu0TqLO7JKeQs7HvKUWp
TB06ipTD0u9csnc4MB7jUckZfHTlxmXOYSmlTb28MAFGguMaNqKYodNTNUKVXp0lUddkhQ
Lvb5zP3KoyZAacFCO/3LEVmvJWCk4eYuLRhG/G52sI2vPiKYXSUMKfTGAccqH1jOu0lZy9
I4in9NJvCnXR2ir3EWoH+PViiXhQev+vA7WnP8VYhVmKf1Wu3W/IyjhDjqKSkPWz+aqlw+
6Ef6B1brmmkaQOKe0V3eQqvNL+VJVLEvz3qqDfeMjLUVbPDsUdBtHxZyWl9Fxg==
ARC-Authentication-Results: i=1; rspamd-86646d89b6-9cnlt;
auth=pass smtp.auth=dreamhost smtp.mailfrom=list1@tompassin.net
X-Sender-Id: dreamhost|x-authsender|tpassin@tompassin.net
X-MC-Relay: Neutral
X-MailChannels-SenderId: dreamhost|x-authsender|tpassin@tompassin.net
X-MailChannels-Auth-Id: dreamhost
X-Tasty-Hysterical: 40aee44312eef779_1698196214406_1582844952
X-MC-Loop-Signature: 1698196214405:928056211
X-MC-Ingress-Time: 1698196214405
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=tompassin.net;
s=dreamhost; t=1698196214;
bh=xFcYN+epc2DTu7JeNXgq5KBUkMRB/graWShiz/uw80c=;
h=Date:From:Subject:To:Content-Type:Content-Transfer-Encoding;
b=G6XKfMfiQLsXyYzycUVPTszePdFgzgU7XtcJmftxm90P22QUdi4oveamMlezQrFEN
qGUDb6C2HFi0TnkEf0kULNh+qZJotxPUzxhy7ibeJF7HevWAiIOrLw7D3UwxHqmkRE
u4aWnoO0XzUzDMbMeS990zHq/6WB9mTidemtrv3ZIV19ZLAH2/0rHSXjkdg72cMoQ8
ADN6Y+JlluQrpO2HCLWXOWKVdt41cD3VPmUweZHbKEkUvA6UId9uTMfis8b4rKBv8Y
RH6MIW82saty8H4nX/r9pNAbdjW7hUj7QSmiN24hZP/tbacjKPm7TzndQCsxF6c3i1
6OzEW1EoImKcA==
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <CAPpdf5_WVe07YVm-dZVV1mpZSWB6v4Z0itRsfYxYVdt8bWt0Ng@mail.gmail.com>
X-BeenThere: python-list@python.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: General discussion list for the Python programming language
<python-list.python.org>
List-Unsubscribe: <https://mail.python.org/mailman/options/python-list>,
<mailto:python-list-request@python.org?subject=unsubscribe>
List-Archive: <https://mail.python.org/pipermail/python-list/>
List-Post: <mailto:python-list@python.org>
List-Help: <mailto:python-list-request@python.org?subject=help>
List-Subscribe: <https://mail.python.org/mailman/listinfo/python-list>,
<mailto:python-list-request@python.org?subject=subscribe>
X-Mailman-Original-Message-ID: <da70b32a-28a3-4a7d-a403-53906cade994@tompassin.net>
X-Mailman-Original-References: <CAPpdf58WXyJs+Rd_GnbS-6dW8bPNt5DsojnVN5_ep+ebNx36Pw@mail.gmail.com>
<58b56dbe-646c-4a94-8102-ac2cf6efe233@tompassin.net>
<CAPpdf5_WVe07YVm-dZVV1mpZSWB6v4Z0itRsfYxYVdt8bWt0Ng@mail.gmail.com>
 by: Thomas Passin - Wed, 25 Oct 2023 01:10 UTC

On 10/24/2023 7:15 PM, o1bigtenor wrote:
> On Tue, Oct 24, 2023 at 6:09 PM Thomas Passin via Python-list
> <python-list@python.org> wrote:
>>
> snip
>>
>> By now you have read many responses that basically say that you cannot
>> prove that a given program has no errors, even apart from the hardware
>> question. Even if it could be done, the kind of specification that you
>> would need would in itself be difficult to create, read, and understand,
>> and would be subject to bugs itself.
>>
>> Something less ambitious than a full proof of correctness of an
>> arbitrary program can sometimes be achieved. The programming team for
>> the Apollo moon mission developed a system which, if you would write
>> your requirements in a certain way, could generate correct C code for them.
>>
>> You won't be doing that.
>>
>> Here I want to point out something else. You say you are just getting
>> into programming. You are going to be making many mistakes and errors,
>> and there will be many things about programming you won't understand
>> until you get some good solid experience. That's not anything to do
>> with you personally, that's just how it will play out.
>>
>> So be prepared to learn from your mistakes and bugs. They are how you
>> learn the nuts and bolts of the business of programming.
>>
>
> I am fully expecting to make mistakes (grin!).
> I have a couple trades tickets - - - I've done more than a touch of technical
> learning so mistakes are not scary.
>
> What is interesting about this is the absolute certainty that it is impossible
> to program so that that program is provably correct.
> Somehow - - - well - - to me that sounds that programming is illogical.
>
> If I set up a set of mathematical problems (linked) I can prove that the
> logic structure of my answer is correct.

In general, that's not the case - CF Godel's Theorem. There are true
arithmetical statements that cannot be proven to be true within the
axioms of arithmetic. There's a counterpart in programming called the
halting problem. Can an arbitrary computer program be proven to ever
finish - to come to a halt (meaning basically to spit out a computed
result)? Not in general. If it will never halt you can never check its
computation.

This doesn't mean that no program can ever be proven to halt, nor that
no program can never be proven correct by formal means. Will your
program be one of those? The answer may never come ...

> That's what I'm looking to do with the programming.
>
> (Is that different than the question(s) that I've asked - - - dunno.)
>
> Stimulating interaction for sure (grin!).
>

1
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor