practal

11 ms·

91.
by practal 2y ago
If you read the baez article, he references a great article by Atiyah, I've posted it: https://news.ycombinator.com/item?id=42989419
92.
Mathematics in the 20th century, by Michael Atiyah [pdf] (2002)(marktomforde.com)
122 points by practal 2y ago|18 comments
93.
by practal 2y ago
I like the weak-link/strong-link distinction, but you need to be careful what problem exactly you are talking about. "Science" is not a problem. "How to distribute funding to scientists" is a problem. And here the w
94.
by practal 2y ago
I am also using AI extensively to discuss my research, for example [1]. And also very excited about AITP (artificial intelligence theorem proving) [2]. [1] A Conversation with Graham Priest About Abstraction Logic. https://practa
95.
by practal 2y ago
No, I was just joking in my last comment, as I know how time-consuming true progress can be. I'm also familiar with how type theory can overcomplicate simple things. When I see this happening, I can't help but point it out, althou
96.
by practal 2y ago
How much work you want to put into understanding abstraction logic is very much up to you. There are no tools for abstraction logic right now. I hope there will be in 15 months ;-) Maybe check back then.
97.
by practal 2y ago
Yes, a type theory is a logic, but not a particularly good one. It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article j
98.
by practal 2y ago
Oh, I like formalising things, don't get me wrong, and I don't mind spending time on it at all. I just don't like doing it via types, and looking at how much time you spent on what, I rest my case.
99.
by practal 2y ago
Stuff like this is why I don't like type systems. What you want to do is easy, but it becomes difficult to explain in a sane way (15 months difficult), because you need to work around the limitations of type systems. When you say &quot
100.
by practal 2y ago
Hi Burak, all serious discussions about types end up talking about logic at some point, and I just don't think that types are a particularly helpful way to think about logic. I'd rather use normal mathematics to think about logic.
101.
by practal 2y ago
Just used this a few days ago to draw a simple diagram [0] for my book [1]! Unfortunately, because it is for category theory only, it doesn't have much support for prettifying your nodes, but you can do that with the latex, of course.
102.
by practal 2y ago
Yes.
103.
by practal 2y ago
Let's just say there is a really big overlap between the two. And each one can learn from the point of view of the other.
104.
by practal 2y ago
> Which is irrelevant, because you can visualize code however you want via editor extensions. Semantically, of course this does not matter. A block is a block, no matter if delineated by indentation or brackets. But RX looks better as pl
105.
by practal 2y ago
> I have more important things to think about in my code than when I switch between two dialects of the language. Granted. The example I gave was just to demonstrate that switching between the styles is not a problem and can be fluid, if
106.
by practal 2y ago
Yes, for a general language (such as abstraction algebra) you would want to allow mixing normal term language and blocks. In RX, that is easy to do: Just reuse the blocks that RX already gives you, while the lines of a block are there for t
107.
by practal 2y ago
In my examples I use RX for the outer structure, which is unproblematic, as RX itself is not complex at all, and parsing it is easy, as easy as parsing brackets. What kind of content you put into the blocks, depends on you. How you parse on
108.
by practal 2y ago
It is obvious to me, nobody would want to represent 35 levels of nesting by indentation. So I would represent the first few (2-4) levels in RX, and the rest by other means, such as brackets. Your language should be designed such that the cu
109.
by practal 2y ago
> S-expressions are the simplest way to linearize a tree. S-expressions are one way to linearize a tree. Now, "simple" can mean different things depending on what you are trying to achieve. RX is simpler than s-expressions if
110.
by practal 2y ago
Recursive teXt (RX) would be a great fit for Lisp, although I am more interested in replacing Lisp entirely with a simpler language rooted in abstraction logic. Note that RX is not like normal semantic white space, but simpler. It is hard c
111.
by practal 2y ago
Assuming this number of indentation is really necessary (which I doubt; maybe a few auxiliary definitions are in order?), obviously only the first few levels would be represented as their own Recursive teXt blocks.
112.
by practal 2y ago
No doubt, brackets of course also convey structure. But I think indentation is better for visualising block structure. Inside these blocks, you can still use brackets, and errors like missing opening or closing brackets will not spill ove
113.
by practal 2y ago
I think simpler is better when it comes to structured editing. Recursive teXt has the advantage that it proposes a simple block structure built into the text itself [1]. Of course, you will need to design your language to take advantage of
114.
by practal 2y ago
This interplay between intuition and logic is exactly what makes the magic happen. You need intuition to feel your way forward, and then logic to solidify your progress so far, and also for ideas maybe not directly accessible via intuition
115.
by practal 2y ago
I'd rather formulate it the other way around. There are not enough smart people in computing working on the really important things. Instead they are working on what pays the most.
116.
by practal 2y ago
Of course term rewriting has a meaning of its own, it is at the same time more meaningful and simpler as any other form of computation.
117.
by practal 2y ago
Yeah, the whole argument felt somewhat unhinged and silly. It is fine to point out that sometimes "function" is used in a more specific manner than "mapping", particularly in analysis, but I doubt any mathematician would
118.
by practal 2y ago
Just to make clear, so you are saying Serge Lang is wrong, too? And as proof you cite various anonymous HN users, most of them heavily downvoted? > I agree it's inaccurate to say it's decided primarily by Foundations vs Analysi
119.
by practal 2y ago
I am looking at the whole development of this thread with amusement, but I also find it somewhat shocking. I see that you are desperately trying to distinguish "foundational" and "analysis" contexts from each other. If y
120.
by practal 2y ago
Try composing f : A -> B with g : A -> B, for A ≠ B. Still, f and g are functions. So, what exactly is your point?

More ›