From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 4.0.1 (2024-03-25) on ip-172-31-91-241.ec2.internal X-Spam-Level: X-Spam-Status: No, score=0.0 required=3.0 tests=none autolearn=ham autolearn_force=no version=4.0.1 Path: nntp.eternal-september.org!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: In precision typing we trust Date: Wed, 27 Aug 2025 09:51:30 +0200 Organization: A noiseless patient Spider Message-ID: <108mde1$gv59$2@dont-email.me> References: <107uv9g$3019a$1@dont-email.me> <107v1ji$303of$1@dont-email.me> <336fbb5f-a279-ea8e-67fd-f62bb00d6a89@irrt.De> <107vfb9$34cpj$1@dont-email.me> <10855lq$gj8l$1@dont-email.me> <1088h1a$19635$1@dont-email.me> <1089p1i$1ig1d$1@dont-email.me> <108aq2p$1qo9o$1@dont-email.me> <108dh2l$2f5h3$1@dont-email.me> <108ej11$2mbr8$1@dont-email.me> <108g1fv$32gqg$3@dont-email.me> <108h6b7$3a75k$3@dont-email.me> <108ijfj$3lihe$4@dont-email.me> <108jqcg$3ti12$2@dont-email.me> <87cy8im3kc.fsf@nightsong.com> <108kp8k$5pr0$1@dont-email.me> <878qj5my4l.fsf@nightsong.com> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Wed, 27 Aug 2025 07:51:30 +0000 (UTC) Injection-Info: dont-email.me; posting-host="27f675d80bb91bc8ee173b07c37e13d3"; logging-data="556201"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/m9BDukg3nNIyiGFWq21cx5nguw+0BM8c=" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:tBewfstq9gtkhoNa3KVm9BoeVJ8= In-Reply-To: <878qj5my4l.fsf@nightsong.com> Content-Language: en-US Xref: feeder.eternal-september.org comp.lang.ada:66938 List-Id: On 2025-08-27 02:00, Paul Rubin wrote: > F didn't encounter a type error until it tried to do arithmetic on its > argument. It didn't encounter error before executing erroneous code... (:-)) > If it instead called its argument based on some decision, > that wouldn't have been a type error. Sure. But this is not a type error, it is untyped. > You don't get to decide whether > that counts as a type system or not. It's just a coarser version of Ada > doing runtime checks on array subscripts and integer overflow, Wrong. Checking constraints is a defined behavior. The type is defined so that exception is a part of the operation's contract. The operation is bounded by that contract. In Python the contract of an operation (if Python were typed) is an open ended and thus non-existent as such. > instead > of statically verifying that they are in range (a proof system like Agda > would consider those to also be type errors). Nope, these are not type errors. In a strongly typed language that thing does not exist per definition because all type errors are detected at compile time. The discussion was whether this would require weakening the type system strength. Python here is really of zero interest. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de