nileshtrivedi

> proof assistants, traditionally, don't use our classic two's complement integers packed into words in our memory, they use Peano numbers

Why can't we just prove theorems about the standard two's complement integers, instead of Nat?

I have now switched to pglite for prototyping, because it lets me use all the postgres features.

This looks useful.

Hope would you say it compares with pgqueuer?

ETA on launching in India?

I don't think it does.

The default Bluesky frontend uses bsky dot app URL when you use the "Copy link to post". Now if one day, you lose trust in this server and switch your PDS, this link continue working depends on this very non-trusted server. If this server is profit-seeking, it can break such links.

An extension or another app is not the solution, and neither is the new at:// URI format, because what matters is the relationship the default server sets up with its majority of users. Most bsky users will lose their traffic to their own posts and therefore will be locked-in, cementing this one server to be the dominant one in all perpetuity. We will therefore get all the patterns of monopolistic abuse that we have seen elsewhere.

Not only is the bluesky network highly centralized right now, its UI is designed to perpetually lock users into the main bluesky server. Even if you use your own identity, when sharing the URLs to the posts via the UI, the URL defaults to bsky dot app domain, which will break if the author ever moves to a second server.

Question since you are here, how long before tool-calling is enabled for Gemma3 models?

I've been thinking on these lines as well. What if computational DAGs spanned boundaries of various machines: the DOM or the UI to client memory to client persisted storage or server memory to database to other connected clients and so on? We seem to be solving the same problems again and again, in various places - mostly in the same way.