back
47 comments
Back when I was in college, I took some philosophy classes just for fun. I discovered when I took Symbolic Logic that while everyone else was struggling with the class, I was finding it pretty easy, because chaining together a proof in symbolic logic felt just like programming. It was the same mental steps: you have the starting conditions, there's an endpoint you want to reach, and you need to chain together these fundamental operations in order to get there. (And sometimes you needed to see how to break them apart: if you need to prove P AND Q, then proving P separately and proving Q separately were usually easier steps, and then once you've proved P and you've proved Q then you've proved P AND Q. Which felt a lot like refactoring a large function that did two things into two separate, smaller functions that do one thing each).

Looking through the sample chapter, I'm reminded of my experience with symbolic logic class. It looks like it'll be much the same thing, but flipped on its head: instead of knowing programming and using that knowledge to make symbolic logic easier, this looks like it'll be about knowing symbolic logic and using that knowledge to make programming easier. Seems pretty useful; I'll give the sample chapters a more in-depth read soon.

Constructing a formal proof is not only related to programming, it's the same thing. Curry–Howard correspondence:

"In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation."

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

It’s not the same thing, in particular if you work in a dynamically-typed programming language, have mutable state, parallelism, and infinite loops. The Curry–Howard correspondence only applies in a limited sense to practical programs.

That’s why you can have a productive programmer who is nevertheless unable to construct valid proofs.

(I’m very much in favor that programming should involve proofs as much as possible, but that’s something to strive for, not a matter of fact.)

The Curry-Howard correspondence applies to all programs and computation, regardless of language. Some languages, such as dynamically typed ones, expose only a higher level abstraction where its inner workings are implicit and hidden (that's the trade-off), so the user of the language cannot work with the actual fundamentals.
Not true. seL4 (for example) is an example of a real time kernel proven correct end-to-end and used on millions of devices.

Another example is CompCert (a proven correct C compiler used by Airbus and others for real production software).

One of the best programmers I ever worked with had a degree in philosophy, having gotten his education before there were formal Computer Science curriculums.

He was one of only two folks I've ever met outside of TeX User Group conferences who had read _The Art of Computer Programming_ (and had a well-thumbed set of Vols. 1--3 on a shelf next to his desk) and had written (and sold commercially) an operating system and full application suite, and when asked, always had a (wonderfully documented) bit of code to apply to any problem.

Ha! Me too - my colleague/friend had a philosophy/political science degree. He was also the funniest person I’ve worked with.

Given the volume of text philosophy wrangles, I’m not surprised TAOCP was casual =))

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 discipline, which are profound. It means that there is no need for classical logic as a separate metalanguage, the properties of programs could also be expressed in the programming language of your choice. Furthermore, it shows that "running the program" and "reasoning about the program" are ultimately the same processes, which raises some good philosophical questions about testing for example. But also about how can we approach the program design, maybe we can just "calculate it" from the constraints. It also opens us to things such as supercompilation.

I think the discipline needs to move towards formal understanding how different programming languages and logics express similar ideas, because it's a really powerful tool of mutual understanding.

(Also, I personally find the typed LC notation, especially with type checking and inference, easier than the classical logic notation. It might be the reason why logic is considered too complicated.)

> I feel like no serious work with this ambition

What ambition? The book is an applied introduction for people who aren’t even familiar with what ∃ means. It’s 200 pages, which is at best comparable to a semester-long course.

Ambition to help programmers understand logic and how it relates to their discipline. But maybe you're right, it cannot be (currently) done in 200 pages, although I hope somebody proves that wrong.

It kinda reminds me of the debate whether functional programming is suitable for beginners, despite being simpler than imperative, while imperative is more familiar.

I am opposed to familiarity argument (I think classical predicate logic and existential quantifier are being taught in early high school, maybe sooner, so they are more familiar than lambda calculus).

Based on my own programming and math experience, I wish I learnt about functional programming, LC, dependent types and CHI much sooner. I don't think it has to be complicated, I know some attempts (although a bit incomplete) to show this to beginners - To Mock a Mockingbird, Haskell Programming from First Principles.

I don't see much value in knowing that dependent types can be used to encode logical quantifiers or similar stuff in applied programming. Maybe there is actual value that it creates after you grok those concepts (beyond the general applicability of any concept or metaphor in your thinking), but I don't see it.

"Functional programming" in applied programming usually just means using less mutable state and using stuff like `map` and `reduce` to make semantics of code more predictable and move the burden of optimizing actual implicit mess it creates to compiler/interpreter.

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.

> 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.
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.

Exactly. There are countless academic books on dry LaTeX logic (logicians love nothing more than writing abstract books about logic) with zero programming applications. But books like this one are very rare.
Looking forward to reading this, I am one of the people who preordered. I've often heard people with degrees say that they regret not being better at the material in this book, so for many peope this will be a chance to practice these skills in a way that their CS/math/physics/engineering degrees didn't really enable.

Also, Hillel (author) has a blog that's absolutely worth checking out as well as some great conference talks which are on YouTube, he's on the short list of speakers who I automatically watch any of their talks.

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. Thx.

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?"

I took some time to think about why this saying bugs me, and I think I've settled on "it suggests you can't understand your limits".

I know it's explaining the joke, but you've blown past "clever" if you've reached the point where you can't debug it.

When you get into team development, doesn't it become the average? So, it's not just about your limits, it's about the team's average.

Otherwise, you're the only one who can fix your code, and becomes a whole bus factor thing.

If debugging is the art of removing bugs from programs, then programming must be the art of inserting them.
This looks great. Most logic books are written by and aimed at mathematicians or philosophers, with basically zero involvement of practical programming applications, while the author here has a software engineering background and it shows.
Congratulations to Hillel for finishing the book!
Thank you for sharing, really appreciate Hillel's content!
I would buy this book, but reading examples of simplify the condition is hard. I don't know the rules that apply to this. Do you know any other book that describes these rules?
I believe that's what the first chapter is for. Kind of a hard problem in deciding what the sample should be, since if it was the first chapter those already familiar with the rules will be disappointed since they want to see applications, but those who don't know the logic rules will have trouble following the applications.
The only one that isn't immediately obvious is https://en.wikipedia.org/wiki/De_Morgan%27s_laws
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).

Alternatively hop straight into Prolog (Art of Prolog, Craft of Prolog).

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

> I'd probably recommend just going with "Introduction to Logic" by Tarski and "Metalogic.

Those are not aimed at programmers, so very different and not a replacement. Just look at the free sample on the website. Besides, incompleteness theorems are probably irrelevant for programmers.

Even though I was doing Prolog (well… Mercury) every day at work, I struggled to get past the first few chapters of Art of Prolog :(

I guess I’m more mature now, so I’ll have yet another attempt… but I don’t like my chances!

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.

Thank you Hillel Wayne. I did the your TLA+ book twice . I am sure this will be a great book.
I would love to support and get a print copy but I just refuse to buy from Amazon.
I'd like to buy this, but when I try to add it to the Leanpub cart, it won't add it.
The problem I see with the book is copy editing. It is self published on lean pub, which I have seen has poor copy editing.
FWIW, I'm on the email list of Hillel, and when discussing that the book is done, he said the following, which makes me thing otherwise:

    This marks the completion of a project that took five years of work, six bookwriting professionals, fourteen domain experts, and fifteen public alphas.

    This has been, without a doubt, the biggest and most exhausting project I've ever done. The examples in the discarded drafts alone could make a second book. The cursed knowledge I've gained on LaTeX and typography could fill a third (or at least a couple of entertaining blog posts). Self-publishing was simultaneously the worst and best decision I made.

    Now excuse me I am going to sleep for a month.
Sleep well, King, you've earned your respite
The footer say HTML code generated by Claude. But who did the css? and who did the js? Tangentially, is html code the correct term if all of it is in a single file or is it still html + css + js code seperately in a single file?
Check the file extension for a static single page app (SPA).

Is it something like .htcsjs, .hsj, or .HSJ on Windows? Or just .html?

More seriously, seems anything that can render .html handles the other two inline, so calling it HTML even with css and js in it seems fine?

I guess my comment came across as if I was mocking the website but I was genuinely curious. And i mean you can have .css filenames and .js filenames in web apps and websites, is that HTML then as well?