From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail From: Paul Rubin Newsgroups: comp.lang.ada Subject: Re: grassroots level SPARK Initiation Date: Thu, 24 May 2018 18:09:12 -0700 Organization: A noiseless patient Spider Message-ID: <87bmd4h77r.fsf@nightsong.com> References: <0cef0914-30b1-4139-a341-40e8f32f85d9@googlegroups.com> <931dc342-50af-4282-baf2-1257d4048da4@googlegroups.com> <87603c4vz6.fsf@nightsong.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: h2725194.stratoserver.net; posting-host="47ec673b7aa730e3380bfb1d027d76e7"; logging-data="11170"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19oDkxHGpBcsPBZs0K/COYC" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:TBKstnhgKFsIh7VGjjLmqlAiH2Y= sha1:lvc+EEbs8bfaLs0IqGy8TKoKB3w= Xref: reader02.eternal-september.org comp.lang.ada:52659 Date: 2018-05-24T18:09:12-07:00 List-Id: Mehdi Saada <00120260a@gmail.com> writes: >> Most math is fundamentally about reasoning about infinite sets. > Except men have been doing math way before last century's mania with > set theory. Yes, usually with the integers (of which there are infinitely many) or else with geometry (lines, planes, or space of infinite size). Set theory itself is much more recent of course. I don't think it's really come up in this discussion except in saying math is about infinite sets, but if you prefer, we could say infinite structures (again the classic example is the integers). > The computer is *never* counting up to the infinite, of > course... It's not *reasoning* about infinite stuff either, it's > always applying a logical, step-by-step recipe, however complex. We're talking about SPARK whose purpose is to prove theorems about programs (that they don't crash, etc). Yes, proving theorems is reasoning. > see NJ.Wildberger, math teacher on YT ... Just be sure this stance > isn't coming from nowhere, nor is devoid of reason. OK, I looked at a couple minutes of video and some of the articles on his web site, and he seems to be espousing some views in the philosophy of mathematics connected with an idea called finitism. That's a little bit off the beaten path, but some good mathematicians such as Edward Nelson have worked in that area. But if you look at http://web.maths.unsw.edu.au/~norman/papers/Ordinals.pdf it's very clear that Wildberger understands the conventional approach perfectly well, so you should learn it too. Also I think he objects to completed infinities (like the ones in set theory) but seems ok with potential infinities (like the integers under the first-order arithmetic axioms). Not allowing completed infinities means we can't collect the integers into a single object, but there is still no largest integer, and we can quantify over the integers to say "every integer has a successor" and things like that. Anyway Enderton's book on logic might mention set theory in a place or two, but it's not really an important part iirc. (He has a separate book on set theory which you might not went to read). You won't encounter set theory much in computer science. In fact the logic used in software proofs is usually intuitionistic logic (aka constructive logic). Not that there's anything wrong with classical logic, but intuitionistic logic happens to work better for the results you want. > I'll look at it. Do you know "HOW TO PROVE IT, A Structured Approach", > from Daniel J. Velleman ? It's lengthier, among other things. It looks like a nice book about doing math proofs, so you should certaintly study it if the stuff in it isn't familiar to you. But it's not a logic book. It might be reasonable to put logic aside temporarily and read Velleman's book first.