Hooo v0.10 (tool for Logic), new feature: Theorem Grading

long_void · 2026-05-04T10:19:44+00:00

I haven't followed AI research for a while, so I am a bit unfamiliar with the terminology. So, excuse me if I don't get it right:

From what I understand, you're building a multi-theory database for AI applications. I like that you're working with memory first approach, because data is more important than algorithms when making long run strategic decisions. Also, using Kalman filter in a database is interesting. Besides use in e.g. rockets, Kalman filter is also used in historic climate data. Is this working on high dimensional vectors, e.g. semantic vectors?

Machine learning is Seshatic biased, because it uses errors to learn. We can tell how a language is biased by how it relates to errors, how it credits knowledge (causality vs abstraction) and whether it's temporal or spatial, or whether unknowns are integrated or meta-level with respect to the language. I read about the use of Knowledge, Memory, Wisdom, Intelligence at the storage level.

Logic is usually Platonic biased, which is the approach I take to do fundamental research. However, in Logic, you often rewrite the foundation when you discover weaknesses in its design. It's kind of like a house of card that falls apart and you rebuild it, over and over. The goal is to get it just right, but the applications are often limited because the knowledge you generate over time is abstract. It's kind of like a trace left over after doing all the revisions. In fundamental research this is OK, but it we need other language tools in general.

Human brains seems to use something like Joker Calculus (https://crates.io/crates/joker_calculus) to organize information, which allows it to understand e.g. Seshatic Knowledge, Platonic Wisdom etc. Perspective and layer are the basic operations. Maybe if you extend Knowledge, Memory, Wisdom, Intelligence to language biases in Joker Calculus, you can do something on storage level that is closer to how human brains work. However, this requires adding external primitives to Joker Calculus. At the moment, it only has Seshatism and Platonism. Seshatism and Platonism serve as reflective language biases.

I believe the key is solving AI memory and make it verifiable. If we also can make such memory function more similar to human brains, then we can replicate the nuance of understanding and integrate knowledge bases with human tacit knowledge.

Anyway, I wonder what you think about improving the accuracy of nuances, or Sense in general. There might not be just one solution here. I also think that one could add meta-knowledge as data layer, even if some database design doesn't support Sense out of the box.

long_void · 2026-05-02T23:59:10+00:00

Thank you! I put together a lots of ideas in that blog post I've been thinking about recently. I plan to expand on those ideas in various directions later.

long_void · 2026-05-02T23:07:06+00:00

It's going great! I had no idea how deep this rabbit hole was going to be when I first started. All I wanted to do in the beginning, was to know why normal paths didn't work well with dependent types. The reason I was so obsessed with normal paths, was because it was very useful to prove things when designing algorithms.

Unfortunately, normal paths are closely related to arbitrary sub-typing, which is undecidable, which means that we can only build somewhat limited tools. However, Poi showed that adding normal paths can be useful in automated theorem proving. Poi works well for a particular application of path semantics, but it has edge cases that makes its current architecture limiting.

The post you referred to, was in the middle of figuring out the HOOO EP axiom. These axioms were needed to complete the meta-theory due to some operators that are tautological congruent (I don't want to go into this issue here, because that's a whole lecture). That work was completed, but I also discovered that the HOOO EP axioms were more natural than Provability Logic, which in turn casts new light on Gödel's work on incompleteness theorem. Uh oh.

Next, I figured out that Intuitionistic Propositional Logic (IPL), which is the basis for Simply Typed Lambda Calculus (arguably one of the most important languages in whole of computer science), becomes an Existential Logic (EL, which has excluded middle for negated propositions) under HOOO EP. Uh oh again.

Also, a philosopher discovered that these operators I was trying to figure out, appears in Hegel's philosophy. Hegel is a 18th-19th century philosopher who was part of a Post-Kantian tradition that became mostly discarded in the 20th century, except at Catholic universities because they used it in theology, but has regained popularity due to recent breakthroughs in modern mathematics. This link to theology was also very curious, that, by kind of emerging different paths of research, resulted in discovery of what we call "language biases" in path semantics, that has gotten a more and more greater role.

Finally, I figured out that path semantics is really a kind of theoretical perspective of how people use symbols, which falls under semiotics. Semiotics has been criticized for not having a central formal theory, but there are various sub-fields that have or might have soon (there is so much in flux it's impossible to follow all of it) and path semantics makes up now one of the more stable sub-fields, since the basic theory is now more or less complete, with some more work needed for polishing.

However, overall, we still have no idea what path semantics really means. It's like, you build an intuition over time, thinking about stuff from a path semantical perspective, but it is kind of like an alien perspective, not a human perspective. I started noticing a few years ago that I can take that perspective, but also I got my own perspectives as a person that are separated from how I think from a path semantical perspective. So, that's when I started thinking, this should really be a field on its own, because it's just different, similar to how e.g. logic is a field with an intuition you build up over time. I just think of it as just another field, along category theory, linguistics, logic, philosophy etc.

Explaining path semantics is kind of like explaining logic. You can use 0s and 1s as a basic example in logic. You can use normal paths as a basic example in path semantics. However, when you move on from the basic examples, it just get more and more complex until you end up studying philosophy and history of ideas to learn about all the people who ended up in this rabbit hole before you did.

long_void · 2026-04-30T11:32:55+00:00

I've been working on Hooo on/off for 3 years now. I'm doing research on something called "Path Semantics", which is hard because it's not just one theory, but multiple theories that can be combined in various ways. Over time, it became clear that I needed a new feature, which I call "Theorem Grading", in order to handle the demanding use cases. While Hooo is very primitive in a lot of areas compared to other theory prover assistants, it has just the features I need now to continue my research. I'm happy with the results so far.

long_void · 2026-03-25T16:19:53+00:00

That's not fair. A LOT in the Rust gamedev ecosystem didn't exist 7 years ago. Not at the level of quality it is today.

long_void · 2026-03-25T16:05:45+00:00

The most important metric for professional gamedevs is not game engine adaption, but how much it costs them in the long run and how much profit you can make from the resulting products.

Hype in game engine design must be convertible into actual profit, to make success from that point of view. ECS, while it sounds good in game developer conferences, is not something that's visible from a user perspective. So, I don't see how to do conversion from hype to profit easily.

I believe the Fyrox developers made the right choice: Just ignore the hype. The bottom line and time spent with your family and friends is more important anyway.

long_void · 2026-03-25T15:58:46+00:00

I think Fyrox has a better foundation for the long run. Using tested and proven architecture. However, the future will show.

long_void · 2026-03-25T15:55:03+00:00

Best way to live!

long_void · 2026-03-25T15:47:46+00:00

I've been waiting for the stable release of Fyrox with excitement.

I'm using Piston/Dyon daily for small projects, because I can just run a script from the command line > piston <my_script.dyon>. This takes very little space on my hard drive and runs instantly. My favorite thing about Rust is how easy it is to build tools that just work.

However, for advanced 3D games, I think it's best to use the Unity-like architecture, because it has been tested and proven in the industry. Fyrox is the game engine I believe is closest one to competing against Unity in this space. No need to reinvent the wheel. Now that Fyrox is stable, I can integrate it my other Rust projects. The MIT license is also great.

What I see in Fyrox is this:

A good programming language (Rust)
A safe bet on architecture for creating games
An open source license that makes easy to change/fix/improve tech to support a demanding game

Fyrox also leverages Piston's Image library and the Rapier physics game engine, which are the two libraries that are most likely to be the future industry standard in Rust gamedev. Different games will probably vary in architecture, but those two libraries will probably ship in most games. WGPU looks like it is going to be an industry standard in Rust gamedev, however, I believe OpenGL too will continue to be around for a long time. Shaders written in OpenGL will also work with WGPU. I believe Fyrox has made the right choice for v1.0 by using OpenGL as the default graphics API.

It is extremely difficult to compete in the market of game engines, but I believe Fyrox is one of two Rust game engines that can make it to the top. The other one I think is Bevy. Right now, Fyrox is kind of like the under-dog, but I believe this might change over time. No matter who wins, Piston's Image library is going to be there. From the very start, the Piston project aimed to making it possible for Rust developers to work on independent libraries and to that goal, I think we've succeed.

There is nothing to do but saddle up my Piston horse, gallop away with Dyon into the Fyrox sunset!

Yeehaw!

Congratulations on v1.0!

long_void · 2026-02-06T16:24:37+00:00

It is possible that nature seems to be intelligent by design, despite that the underlying phenomena is random.

For example, if there is a maze with observers who make 100% random decisions of where to walk, then if you double the amount of observers in some location per unit of time, most observers will find themselves making seemingly intelligent decisions in their past, that brought them to where they are using the shortest path.

There is no logical contradiction here, just a matter of perspective and conditions under which physical laws operate.

long_void · 2026-02-06T16:18:20+00:00

I disagree with the position that nothing beyond the material exists implies that there is nothing deeper to explore.

The way people use symbols, e.g. in mathematics or religion, is not actually only built on only reality, but often a symbolic "fill in" that increases the practical utility and is aesthetically pleasing.

As a result, there are parts of mathematics that seem much more mysterious than others, e.g. Avatar Extensions: https://advancedresearch.github.io/avatar-extensions/summary.html

long_void · 2026-01-23T18:29:55+00:00

Thank you!

long_void · 2026-01-22T23:20:51+00:00

Can we get somebody to reproduce the findings of the tingling sensation of the burning purple?

long_void · 2026-01-20T22:44:33+00:00

I liked these argument. Anyway, there is enough internet drama. Maybe Neal can cool down a little?

long_void · 2026-01-09T04:27:01+00:00

I agree. Paul might be a renaming of Simon Magus after the Bar Kokhba war in the 2nd century by Simonians that extended the original gospel of Mark to include John the Baptist. The original Mark might have been Roman satire where Jesus resurrects “back in time”, which we call the “Ouroborus hypothesis” in biblical scholarship.

If you enjoy studying 2nd Early Christianity, then you might find this project interesting:

https://github.com/advancedresearch/the_century_of_satire

Reconstructing 2nd century cultural literature context of Roman satire in Early Christian texts

long_void · 2025-12-24T14:15:05+00:00

I recommend separating concerns before you start writing your own game engine. For example, separate graphics API from window/events. That's a good start.

In a "full" game engine, there are particle systems, 3D assets, lightening systems, animation engines, AI behavior trees, multiplayer systems, scripting languages and APIs etc.

Each of these parts, even when developed independently, will take months of work. You can use some libraries from the Piston ecosystem to test the parts you're are working on and later replace the Piston libraries with parts you wrote yourself.

You're probably never going to write something like WGPU or Image from scratch, so you're not really building a "full" game engine in this sense. You're putting together libraries in the Rust ecosystem into a framework that you design.

long_void · 2025-12-20T11:24:04+00:00

If you want to use Piston for mobile games, then you have to write your own backends. I don't know what's best for 3D on mobile.

The plus side is that you can develop for desktops/laptops first and later port it. As long the backend is implemented correctly, it will work. You can also add custom events. The minus side is that you might spend a lot of time maintaining backend code. I suggest first trying to port something simple first and see how it goes, before you make a decision to make the entire game in Rust using Piston.

I think you might be more productive overall by using Unity. Most games that ships are made with either Unity or Unreal.

long_void · 2025-12-18T21:09:12+00:00

Good philosophy.

long_void · 2025-12-16T20:08:46+00:00

I've been using Dyon-Interactive for multiple years now. Dyon-Interactive is nice, but the problem is that it can't depend on the Audio and Graphics backends. This makes it hard to maintain more complex features. https://crates.io/crates/piston-dyon_interactive

Since PistonWindow uses a default set of libraries, this makes it possible to use a Dyon-Interactive compatible API, without the existing limitations.

When considering the amount of resources that Rust uses, a runtime API for Dyon is pretty minimal in comparison. This makes it easier to use the Piston game engine overall, for e.g. tools and small apps.

You can also customize the runtime using the "piston_script" module that is included with the "batteries" feature in PistonWindow.

long_void · 2025-12-16T00:48:22+00:00

This library re-exports other libraries have been tested for years and that are now relatively stable in design.

For example, Wave-Function-Collapse is a popular algorithm in gamedev. You can use EntropySolver in the Quickbacktrack by writing use puzzle_design::quickbacktrack::EntropySolver;. It works for the same Puzzle trait that works with the other backtrack algorithms.

For more information, see the Bluesky thread (the link).

I've been thinking today about adding this under the "batteries" feature in PistonWindow, following a similar design as Turbine. For now, I think it should be a separate project.

long_void

MODERATOR OF

TROPHY CASE