>The logical calculus is easier to execute than any of the techniques of mathematics itself, yet only in 1934 did Gerhard Gentzen set it out in a natural way. Even now, mathematics students are expected to learn complicated (epsilon, delta)-proois in analysis with no help in understanding the logical structure of the arguments. Examiners fully deserve the garbage that they get in return.
With an opening like that how can I not read the rest of the book?
This actually touches on some work I've been doing the past week - arbitrary term rewriting to test how reliable a given LLM is when it needs to reason about symbolic manipulation. Everything is dynamically generated to avoid the usual problem of memorising every validation set every llm seems to suffer from.
I am interested in this problem as well. Please share any notes.
I am attempting to create parameterized "logic" problems (similar to the zebra puzzle) which cannot be solved by LLMs even when they are trained on it, or even when they "reason" on it.
Meanwhile this approach is even simpler, where it is demonstrated that LLMs cannot recognize 3 state DFAs. https://arxiv.org/pdf/2501.02825
This was paid work until recently but the start up pivoted to something else and now I'm wondering what to do with code that takes a few thousand dollars to run every time and is of questionable copyright ownership.
A someone interested in programming language theory, this book looks very interesting. Unfortunately the HTML is incomplete and very hard to read, and the book itself is quite expensive.
This is up there with The Art of Computer Programming for me as a text that has clearly been painstakingly crafted by its author. It shares as well with TAOCP that it is simultaneously so many things: an introduction to programming language semantics, an introduction to category theory, (in later chapters) a reference on pretty sophisticated programming language semantics, and an exploration of the rich connections between all of these topics. I owe huge chunks of my bachelor's thesis [1] to Paul and I eagerly look forward to returning to his text after my retirement from software engineering :)
This book is for you if:
- You have some exposure to PL semantics (lambda calculus, functional programming) in the operational tradition.
- You have some background in abstract algebra and/or category theory.
- You have neither but you're interested and willing to grind.
A word on the title: the contents are practical for doing mathematics; if you're interested in studying lambda calculi and want fancy techniques for writing light, elegant proofs about their properties, this is a great resource. If you're into building systems it may not be as useful to you.
With llms and theorem provers doing the formalism, what is left is intuition - love the intuitionist focus in this book, also tying into what Bessis said in [1]
I intend to read this book in depth.
The practical application of these foundations is the field of programming language theory. At least that is the application I know of.
Whether programming language theory is practical or not depends, I think, on your attitude to programming languages. For example, if you think C is a masterpiece of clean and elegant design I suspect you won't have much time for programming language theory. If you think C is riddled with mistakes, then you will find solutions in programming language theory.
You do understand how a mathematical Theory (a set of true propositions made by relating operations i.e. from axioms and inference rules) and a Model (a set of elements with all the operations defined and where all the propositions are true) are related, i presume?
PLT is not one theory but a set of theories from which you are free to pick and choose any subset you would like to model in your language's abstract machine and syntax/semantics.
C simply chose a "minimal theory" and there is nothing wrong with that.
C arguably doesn't actually have formal semantics, the struggles of the standard committee trying to figure out the pointer provenance being one obvious example.
C does have formally defined semantics as given by the standard but chose to leave some open-ended to give compiler writers more freedom in the form of a) Unspecified behaviour b) Implementation defined behaviour and c) Undefined behaviour.
>The logical calculus is easier to execute than any of the techniques of mathematics itself, yet only in 1934 did Gerhard Gentzen set it out in a natural way. Even now, mathematics students are expected to learn complicated (epsilon, delta)-proois in analysis with no help in understanding the logical structure of the arguments. Examiners fully deserve the garbage that they get in return.
With an opening like that how can I not read the rest of the book?
This actually touches on some work I've been doing the past week - arbitrary term rewriting to test how reliable a given LLM is when it needs to reason about symbolic manipulation. Everything is dynamically generated to avoid the usual problem of memorising every validation set every llm seems to suffer from.
Anything public you can share yet? I’ve been interested in how much LLMs “understand” symbolism.
I am interested in this problem as well. Please share any notes.
I am attempting to create parameterized "logic" problems (similar to the zebra puzzle) which cannot be solved by LLMs even when they are trained on it, or even when they "reason" on it.
Meanwhile this approach is even simpler, where it is demonstrated that LLMs cannot recognize 3 state DFAs. https://arxiv.org/pdf/2501.02825
You can email me if you're interested.
This was paid work until recently but the start up pivoted to something else and now I'm wondering what to do with code that takes a few thousand dollars to run every time and is of questionable copyright ownership.
A someone interested in programming language theory, this book looks very interesting. Unfortunately the HTML is incomplete and very hard to read, and the book itself is quite expensive.
Have you read TAPL? I bought the physical copy and found it 100% worth it. Really easy to work through, even with a layperson's understanding of math
[1] https://www.cis.upenn.edu/~bcpierce/tapl/
I noticed this. When reding about denotations the cent sign appears. What do you suppose it actually should be ?
This is up there with The Art of Computer Programming for me as a text that has clearly been painstakingly crafted by its author. It shares as well with TAOCP that it is simultaneously so many things: an introduction to programming language semantics, an introduction to category theory, (in later chapters) a reference on pretty sophisticated programming language semantics, and an exploration of the rich connections between all of these topics. I owe huge chunks of my bachelor's thesis [1] to Paul and I eagerly look forward to returning to his text after my retirement from software engineering :)
This book is for you if:
A word on the title: the contents are practical for doing mathematics; if you're interested in studying lambda calculi and want fancy techniques for writing light, elegant proofs about their properties, this is a great resource. If you're into building systems it may not be as useful to you.[1] https://github.com/jaykru/thesis/blob/trunk/thesis.pdf
https://www.artima.com/shop/modern_mathematics may be of interest to people too.
With llms and theorem provers doing the formalism, what is left is intuition - love the intuitionist focus in this book, also tying into what Bessis said in [1] I intend to read this book in depth.
Author: please fix the html rendering.
[1] https://www.amazon.com/Mathematica-Secret-World-Intuition-Cu...
For folks looking - The pdf you can find/buy has the math correctly rendered
https://www.amazon.com/Practical-Foundations-Mathematics-Cam...
200$ for correct latex
Looking at the table of contents, this seems like a really odd title. In what sense is this practical and a foundation for mathematics?
> In what sense is this practical and a foundation for mathematics?
in a strong computational sense
Ah, now it makes sense, thanks! I was misinterpreting "of" as "for".
It's "practical" for the academic. Everyone else should just get a discrete math book and work through the first few chapters.
Practical in the same sense as André Weil's book on number theory is basic :)
I think the author assumes u know how to apply a practical foundation. We need another book here.
The practical application of these foundations is the field of programming language theory. At least that is the application I know of.
Whether programming language theory is practical or not depends, I think, on your attitude to programming languages. For example, if you think C is a masterpiece of clean and elegant design I suspect you won't have much time for programming language theory. If you think C is riddled with mistakes, then you will find solutions in programming language theory.
You do understand how a mathematical Theory (a set of true propositions made by relating operations i.e. from axioms and inference rules) and a Model (a set of elements with all the operations defined and where all the propositions are true) are related, i presume?
PLT is not one theory but a set of theories from which you are free to pick and choose any subset you would like to model in your language's abstract machine and syntax/semantics.
C simply chose a "minimal theory" and there is nothing wrong with that.
C arguably doesn't actually have formal semantics, the struggles of the standard committee trying to figure out the pointer provenance being one obvious example.
C does have formally defined semantics as given by the standard but chose to leave some open-ended to give compiler writers more freedom in the form of a) Unspecified behaviour b) Implementation defined behaviour and c) Undefined behaviour.
https://news.ycombinator.com/item?id=20168936 probably will do the trick?