practal

8 ms·

61.
by practal 1y ago
I think it is available on Claude Pro now, so just $20.
62.
by practal 1y ago
Gödel's incompleteness theorem tells you why it is a good idea to separate semantics (notion of truth) from syntax (reasoning). Because some things are true, although you cannot prove that they are. Some people now put forward from thi
63.
by practal 1y ago
I asked him more than 10 years ago if he would be interested in a formalisation of the proof, and he politely declined. I guess he was right to decline, my proposal would not have been viable then anyway.
64.
by practal 1y ago
I am wondering how much this "prove isomorphism to Mathlib equivalent" is relevant. By this I mean, would anything change if the isomorphism part would be left out, i.e. is it actually used anywhere, for example for automatically
65.
by practal 1y ago
De Bruijn indices are great, I use them to construct what I call the "De Bruijn Abstraction Algebra"; it comes in two forms, one is used to give a characterisation of alpha equivalence for abstraction algebra, the other one is use
66.
by practal 1y ago
What is bombastic about them?
67.
by practal 1y ago
Strong opinion! Also, it seems you didn't read my interaction so far carefully enough. You also didn't read the summary I linked to, otherwise you would know that I fully approve the current use of types in programming languages,
68.
by practal 1y ago
What is the type of x / y, for x : ℝ and y : ℝ?
69.
by practal 1y ago
I routinely describe code that I want in natural language, and it generates correct TypeScript code for me automatically. When it gets something wrong, I see that it is because of missing information, not because it is not smart enough. If
70.
by practal 1y ago
Given that I am an Isabelle user and/or developer since about 1996, similarities with Isabelle are certainly not accidental. I think Isabelle got it basically right: its only problem (in my opinion) is that it is based on intuitionisti
71.
by practal 1y ago
There is nothing practically usable right now. I hope there will be before the end of the year. Algebraic effects seem an interesting feature to include from the start, they seem conceptually very close to abstraction algebra.
72.
by practal 1y ago
I have not defined any "abstract lattice extension" explicitly; which is nice, why would I need to know about lattices for something as simple as this? It is just a convention I suggest to get a useful Defined predicate, actually.
73.
by practal 1y ago
You seem to know AL very well, I didn't even know that there is a computational interpretation of AL proofs! Can you tell me what it is?
74.
by practal 1y ago
Saying "Curry-Howard, Curry-Howard, Curry-Howard" isn't an argument, either. I am not saying that types cannot do this work. I am saying that to do this work you don't need types, and AL is the proof for that. Well, firs
75.
by practal 1y ago
Yes and no. Yes, predicates are more flexible, because they can range over the entire mathematical universe, as they do for example in (one-sorted) first-order logic. No, names are not a problem, predicates can have names, too.
76.
by practal 1y ago
Types for real-world semantics are fine, they are pretty much like predicates if you understand them like that. The idea to use predicates instead of types has been tried many times; the main problem (I think) is that you still need a nice
77.
by practal 1y ago
I think I have a reference to Curry in my summary link. Anyways, curry-howard is a nice correspondence, about as important to AL as the correspondence between the groups (ℝ, 0, +) and (ℝ \ 0, 1, *); by which I mean, not at all. But type peo
78.
by practal 1y ago
Practically, in abstraction logic (AL) I would solve that (AL is not a practical thing yet, unlike TLA+, I need libraries and tools for it) by having an error value ⊥, and making sure that abstractions return ⊥ whenever ⊥ is an argument of
79.
by practal 1y ago
I've summarized my opinion on this here: https://doi.org/10.5281/zenodo.15118670 In normal programming languages, I see static type systems as a necessary evil: TypeScript is better than JavaScript, as long as you
80.
by practal 1y ago
Algebraic effects seem very interesting. I have heard about this idea before, but assumed that it somehow belonged into the territory of static type systems. I am not a fan of static type systems, so I didn't look further into the idea
81.
by practal 1y ago
Obligatory: https://claude.ai/referral/YWAsr_1fbA
82.
by practal 1y ago
Ok, so the main point that makes it different from CRDTs seems to be: if you have a central server, let the server do the synchronization (fixing an order among concurrent events), and not the data structure itself via an a-priori order. Be
83.
by practal 1y ago
This is the spec that counts: https://github.com/modelcontextprotocol/modelcontextprotocol... How exactly those messages get transported is not really relevant for implementing an mcp server, and easy to switch, as lon
84.
by practal 1y ago
The difficult part is figuring out what kind of abstractions we need MCP servers / clients to support. The transport layer is really not important, so until that is settled, just use the Python / TypeScript SDK.
85.
by practal 1y ago
There isn't much detailed technical spec on MCP on the spec site, but they have a link to a schema [1]. You can add that schema to a Claude project, and then examine it. That's very helpful, although you will quickly run into unsu
86.
by practal 2y ago
I clean offices for three hours a day to pay for my research. Beats using my brain for something somebody else is interested in, but I am not! Each time somebody buys my book [1], I convert it mentally into hours of cleaning :-) [1] http:&
87.
by practal 2y ago
Fair enough. My personal motivation is abstraction logic (AL), and one way of viewing it is as a generalisation of equational reasoning. I am just starting to implement rewriting for AL, but I will definitely drop you a line once you can pl
88.
by practal 2y ago
Such a database of rewrite rules only doesn't make much sense because the semantic part is missing (what does a rule mean, and why is it correct?), and so you will run into inconsistencies quickly as the database grows. But if you take
89.
by practal 2y ago
Love the von Neumann "aufgewärmte Suppe" anecdote.
90.
by practal 2y ago
Lots of interesting thoughts and insights in that article. I find it especially interesting to relate Geometry to Space, and Algebra to Time.

More ›