practal

What is bombastic about them?

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, as they provide lightweight formal methods (another name for what you call "fast, formal checking"). But I think we will be able to do much better, we will have fast, formal checking without static types. Not today, not tomorrow, but certainly not more than 10 years from here.

What is the type of x / y, for x : ℝ and y : ℝ?

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 I needed any more evidence for Strong AI since AlphaGo, that would be it.

I wouldn't call it vibe coding; I just have much more time to focus on the spec than on the code. I'd call that a sufficiently smart compiler.

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 intuitionistic type theory as a metalogic and not abstraction logic (nevertheless, most type theorists pretty much ignored Isabelle!). Abstraction logic has a simple semantics; ITT does not. My bet is that this conceptual simplicity is relevant in practice. We will see if that is actually the case or not. I've written a few words about that in the abstraction logic book on page 118, also available in the sample.

> — a notational reshuffling of well-trod ideas in type theory

Always fun to encounter disparaging comments (I see that you deleted the other one in the other thread), but I wrote this answer more for the other readers than for you.

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.

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. Nobody can stop you from defining mul 0 ⊥ = 0, for example, and that might make sense sometimes.

I would suggest that abstraction logic compares to type theory as Lisp compares to Standard ML; but that is just an analogy and not precise.

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?

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, first-order logic is already the proof for that, but it doesn't have general binders.

Now, you are saying, whenever this work is done, it is Curry-Howard, but that is just plain wrong. Curry-Howard has a specific meaning, maybe read up on it.

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.

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 way of binding variables, and types seem the only way to do so, so you will introduce types anyway, and what is the point then? The nice thing about AL is that you can have a general variable binding mechanism without having to introduce types.

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 people like bringing it up even when it is not relevant at all.

No, sorry, I really don't have types. Maybe trying to reduce all approaches to logic to curry-howard is the very reductive view here.

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 the abstraction, or when the return value is otherwise not well-defined [1]. For example,

    div 7 0 = ⊥, 

and

    plus 3 ⊥ = ⊥, 

so

    plus 3 (div 7 0) = ⊥.

In principle, that could be done in TLA+ as well, I would guess. So you would have to prove a predicate Defined, where Defined x just means x ≠ ⊥.

[1] Actually, it is probably rather the other way around: Make sure that if your expression e is well-defined under certain preconditions, that you can then prove e ≠ ⊥ under the same preconditions.

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 don't confuse types with terms...

But in a logic, types are superfluous: You already have a notion of truth, and types just overcomplicate things. That doesn't mean that you cannot have mathematical objects x and A → B, such that x ∈ A → B, of course. Here you can indeed use terms instead of types.

So in a logic, I think types represent a form of premature optimisation of the language that invariants are expressed in.

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.

But I found these two articles [1] about an earlier dynamic version of Eff (the new version is statically typed), which explains the idea nicely without introducing types or categories (well, they use "free algebra" and "unique homomorphism", just think "terms" and "evaluation" instead). I find it particularly intriguing that what Andrej Bauer describes there as "parameterised operation with generalised arity", I would just call an abstraction of shape [0, 1] (see [2]). So this might be helpful for using concepts from algebraic effects to turn abstraction algebra into a programming language.

[1] https://math.andrej.com/2010/09/27/programming-with-effects-...

[2] http://abstractionlogic.com

Obligatory: https://claude.ai/referral/YWAsr_1fbA

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.

Because all communication is between client and server, and never between clients, when the client connects to the server, the server can make sure that it first processes all of the client's local operations before sending it new remote updates.

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 long as there is some standard.

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.

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 unsupported things, for example embedded resources in tool call responses in Claude Desktop.

I think MCP will be a huge deal for Practal. Implementing Practal as an MCP server, I basically don't need a frontend.

[1] https://github.com/modelcontextprotocol/modelcontextprotocol...

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://abstractionlogic.com

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 play around with it. Maybe AL can be your common format, instead of just a 15th engine for it :-) There are two reasons why I think that:

1. AL is more general than first-order rewriting, because it has general binders, that is general variable binding constructs.

2. Unlike higher-order logic, which also has general binders, it doesn't have types, so rewrite rules in AL can be taken for face value, and have no hidden type annotations in them, just like in first-order rewriting (that is a consequence of AL having a single mathematical universe).

I must admit, I am quite excited about implementing rewriting for AL! My PhD father has co-authored a book about (mostly) first-order term rewriting [1]. Higher-order rewriting based on the lambda calculus is mentioned briefly in it (and of course implemented in Isabelle), and I am wondering if rewriting based on AL instead will bring new insights and/or techniques.

[1] Term Rewriting and All That. https://doi.org/10.1017/CBO9781139172752

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 the idea of a universal system for rewrite rules seriously, and add just enough semantics to make it work as a logic, you might arrive at abstraction logic [1]. That is actually a great way of explaining abstraction logic to computer scientists, come to think of it!

[1] http://abstractionlogic.com

Love the von Neumann "aufgewärmte Suppe" anecdote.

Lots of interesting thoughts and insights in that article. I find it especially interesting to relate Geometry to Space, and Algebra to Time.

If you read the baez article, he references a great article by Atiyah, I've posted it: https://news.ycombinator.com/item?id=42989419

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 weakest links actually matter, because you only have a finite amount of funding, and you don't want to waste it on the weak scientists, so you have more for strong scientists.

Another way of phrasing that problem is, "what actually is strong science, and what is weak science"? Over a few decades, that question usually plays out correctly, but even a few years is often not enough to tell, even for specialists, especially for truly new and original science. As an example, right now, would you say abstraction logic [1] is strong or weak science?

And of course, venture capital funding is also not a strong-link problem. You can waste money on some weak startups that you thought were actually strong, but do that too much, and your fund goes under.

[1] http://abstractionlogic.com

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://practal.com/press/cwgpaal/1

[2] Abstraction Logic Is All You Need. https://doi.org/10.5281/zenodo.14737457

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, although my criticism might seem out of context. I would be very happy if I could deliver tools for abstraction logic in just 15 months.

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.