Comment by js8 | Hacker News Reader

Comment by js8 | Hacker News Reader

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.

Reply on news.ycombinator.com