Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Logic for Programmers

logicforprogrammers.com

Post reply on HN
Print view View original

21–30 of 53 posts

Re: Logic for Programmers

#21

Post by epolanski »

I was waiting for the longest time for Hillel to finish his book, I don't like early drafts, glad he's completed it!

Reading some comments in this thread is borderline depressing: half of the people complaining this isn't more abstracted and generalized mathematics and the other half complaining there's too much computer science and is not about coding only.

Which means that this book is exactly perfect for programmers interested in learning about computer science. Might be a niche, but it is a real audience.

Re: Logic for Programmers

#22

Post by epolanski »

js8 wrote: post #16

Looks like a nice book, but.. I feel like no serious work with this ambition today should omit (maybe it is present, not sure from the ToC) the Curry-Howard isomorphism, propositions-as-types, and from it following the analogy between logics and lambda calculi. I really like this: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.... I think every programmer should understand the consequences of CHI to the…

> It means that there is no need for classical logic as a separate metalanguage

I'm not following your point, is the criticism that a book on logic is only focusing on logic?

Re: Logic for Programmers

#23

Post by foobarbecue »

Trying to buy this on Amazon seems to trigger a bug.

If I do "buy now," I get a strange text-only "out of stock" page.

If I add to cart and try to check out, I'm redirected to the "switch account" page, where only my currently logged-in account is listed.

I buy things on amazon ask the time and have never seen this before.

EDIT: whatever that was, it's fixed now. I was able to purchase the print book.

Re: Logic for Programmers

#26

Post by xelxebar »

fmajid wrote: post #12
kriro wrote: post #8

Looking at the table of contents, I see no mention of Gödel/incompleteness theorems or limitations which is not a great sign. It does look well structured though but I'd probably recommend just going with "Introduction to Logic" by Tarski and "Metalogic. An introduction to the metatheory of standard first order logic." by Hunter. Those served me well and are fairly understandable for a non-mathematician (imo). Altern…

How are Gödel's incompleteness theorem relevant to the working programmer?

Programs as data.

Proofs of incompleteness theorems, the halting problem, Rice's theorem etc. all share a diagonalization structure. The keyword here is Lawvere's fixed-point theorem[0], but it's a bit of abstract nonsense, so here's a good accessible video on the topic[1].

I'm not sure the incompleteness theorems themselves are immediately and directly applicable to software development, but I find that having several examples of diagonaization proofs bouncing around in my head makes the Lawvere structure apparent. Since proofs are just programs, the pattern is surprisingly pervasive. Futamura projections are one incarnation, which is essentially how many interpreters end up providing "compilation" of programs into standalone binaries.

[0]:https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theore...

[1]:https://www.youtube.com/watch?v=dwNxVpbEVcc

Re: Logic for Programmers

#27

Post by js8 »

cubefox wrote: post #19
js8 wrote: post #16

Looks like a nice book, but.. I feel like no serious work with this ambition today should omit (maybe it is present, not sure from the ToC) the Curry-Howard isomorphism, propositions-as-types, and from it following the analogy between logics and lambda calculi. I really like this: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.... I think every programmer should understand the consequences of CHI to the…

The book you mention is the opposite of "Logic for Programmers": it's abstract academic mathematics with zero code. (Except in the sense that constructive proofs are allegedly code. They are not, unless they are written in an actual programming language like Lean.)

Yes, it's an academic work. But that's my point, somebody should popularize it among programmers, because the understanding of correspondence between a programming language and the metalogic we use to describe the problem (even when we talk to LLM for instance) has consequences how you approach programming.

"constructive proofs are allegedly code. They are not"

I disagree, what CHI shows is that specific language you choose matters only a little (as long as you stick to TC and have some means of compositionality).

I want programmers get to the point where they think of programming in a single unified language, of which different programming languages (and logics) are just expressions of (sometimes a bit more restrictive). I think it would enable metaprogramming (and formal methods) on an unprecedented scale.

Re: Logic for Programmers

#29

Post by js8 »

epolanski wrote: post #22
js8 wrote: post #16

Looks like a nice book, but.. I feel like no serious work with this ambition today should omit (maybe it is present, not sure from the ToC) the Curry-Howard isomorphism, propositions-as-types, and from it following the analogy between logics and lambda calculi. I really like this: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.... I think every programmer should understand the consequences of CHI to the…

> It means that there is no need for classical logic as a separate metalanguage I'm not following your point, is the criticism that a book on logic is only focusing on logic?

Well, I was inspired by the top comment which said "doing logic surely feels like programming". Not a coincidence, they are a very same thing - CHI. Book on logic shouldn't beat around that bush (because frankly, mathematicians know better than programmers); it should address it head on, that using classical logic as a metalanguage in programming is more of a historical accident, and we could use pretty much any programming language as well. Which means at least some metalogical reasoning could be and should be automated, an interesting fact for any working programmer.

Re: Logic for Programmers

#30

Post by rswail »

jpollock wrote: post #9
Merkur wrote: post #5

I read the free part. Looks interesting, but the math heritage is dominant as promised. It seems to favor the compact and efficient kind of code that is brittle in the hand of a mildly competent junior dev, or a heavy multitasking senior. I like smart code, in fun projects, but on the job I prefer fast to read and to reason code. Don’t try to be fancy. So I guess that’s a book to challenge my assumptions. I like that…

I know that as Kernighan's Law. Seems to be something that seniors learn over time. https://github.com/dwmkerr/hacker-laws#kernighans-law "Everyone knows that debugging is twice as hard as writing a program in the first place. So if you're as clever as you can be when you write it, how will you ever debug it?"

If debugging is the art of removing bugs from programs, then programming must be the art of inserting them.
Post reply on HN