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 <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: grassroots level SPARK Initiation
Date: Thu, 24 May 2018 13:52:45 -0700
Organization: A noiseless patient Spider
Message-ID: <87603c4vz6.fsf@nightsong.com>
References: <0cef0914-30b1-4139-a341-40e8f32f85d9@googlegroups.com>
	<931dc342-50af-4282-baf2-1257d4048da4@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: h2725194.stratoserver.net;
 posting-host="dc85dea2bd14aaf6b0b2f2eef61c4633";
	logging-data="15254"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+UcoVpjjTGeYxNrL5u4CtP"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:2Ub/BqfDynxSa7tUqLa5ri9dKO4=
	sha1:xQxXu24knI5yUqFqT8ypJ8mnJjo=
Xref: reader02.eternal-september.org comp.lang.ada:52650
Date: 2018-05-24T13:52:45-07:00
List-Id: <comp.lang.ada>

Mehdi Saada <00120260a@gmail.com> writes:
> I am trying both Gries' Science of Programming and Enderton's
> introduction to logic.... I quickly hated the second as, as has been
> said, it's QUITE not the right orientation, indeed.  It casts
> everything in nonsensical mumbo-jumbo (to be polite ;-) ) whereas a
> down-to-earth - and finitist - approach would use primarily basic
> field agebra, multisets and operations on them to model logical
> reasoning.

Most math is fundamentally about reasoning about infinite sets, such the
integers.  The area within math that deals with finite sets is called
combinatorics and it is hard.  SPARK almost certainly deals with
infinite models.  You might want to prove that a function never crashes
for any sequence of inputs, so you have to quantity over all possible
sequences, of which there are infinitely many.

Finiteness actually makes things harder.  Like if you write a program
that does some calculations with integers, you can prove the algorithm's
correctness using the rules of arithmetic (commutative law, induction,
bla bla bla).  E.g. maybe the algorithm computes some number N and then
does something with its successor N+1.  In math that is fine, every
number has a successor, but that's because the integers are an infinite
set.  If you want to stay with finite sets, you can't say "ok I have N
so I'll compute N+1 and use it for whatever".  You have to *also* prove
that N is small enough that computing N+1 won't result in arithmetic
overflow.

I guess I can sympathize if you didn't like Enderton's book.  I liked it
but I agree that it used a lot of weird symbols whose meanings took
getting used to, etc.  Plus, it's possibly too oriented towards abstract
math and maybe even philosophy.  It's been a long time since I used it
so maybe I'm forgetting.  I typed "logic for computer science" into web
search and found tons of plausible looking books.  Maybe you could try
one of those.

Wikipedia has an article on natural deduction, though I don't know how
it compares with whatever you looked at:

https://en.wikipedia.org/wiki/Natural_deduction

See if you like this better than Enderton's book (it is less mathematical):

https://www.fecundity.com/codex/forallx.pdf
Info page: https://www.fecundity.com/logic/