[HN Gopher] Practical Foundations of Mathematics
___________________________________________________________________
Practical Foundations of Mathematics
Author : nill0
Score : 109 points
Date : 2025-02-24 13:24 UTC (3 days ago)
(HTM) web link (www.paultaylor.eu)
(TXT) w3m dump (www.paultaylor.eu)
| noelwelsh wrote:
| 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.
| whitten wrote:
| I noticed this. When reding about denotations the cent sign
| appears. What do you suppose it actually should be ?
| shpongled wrote:
| 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/
| revskill wrote:
| I think the author assumes u know how to apply a practical
| foundation. We need another book here.
| WildRyc wrote:
| https://news.ycombinator.com/item?id=20168936 probably will do
| the trick?
| noelwelsh wrote:
| 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.
| rramadass wrote:
| 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.
| Joker_vD wrote:
| 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.
| llm_trw wrote:
| >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.
| memhole wrote:
| Anything public you can share yet? I've been interested in how
| much LLMs "understand" symbolism.
| bwfan123 wrote:
| 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
| llm_trw wrote:
| 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.
| jebarker wrote:
| Looking at the table of contents, this seems like a really odd
| title. In what sense is this practical and a foundation for
| mathematics?
| ysofunny wrote:
| > _In what sense is this practical and a foundation for
| mathematics?_
|
| in a strong computational sense
| jebarker wrote:
| Ah, now it makes sense, thanks! I was misinterpreting "of" as
| "for".
| zero-sharp wrote:
| It's "practical" for the academic. Everyone else should just
| get a discrete math book and work through the first few
| chapters.
| dorian-graph wrote:
| https://www.artima.com/shop/modern_mathematics may be of interest
| to people too.
| esafak wrote:
| Practical in the same sense as Andre Weil's book on number theory
| is basic :)
| bwfan123 wrote:
| 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...
| aerioux wrote:
| For folks looking - The pdf you can find/buy has the math
| correctly rendered
|
| https://www.amazon.com/Practical-Foundations-Mathematics-Cam...
___________________________________________________________________
(page generated 2025-02-27 23:01 UTC)