You can. Naturals are the default because the kinds of people who write and use proof assistants think usually in terms of natural numbers first rather than the 2-adic numbers mod 2^N we use in programming, or even the plain 2-adics used for algorithmics. It's like mathematicians and 1-based indexing. It violates programming conventions, but the people using it find it easier.
`pglite` is a WASM version of postgres. I use it in one of my side projects for providing a postgres DB running in the user's browser.
For most purposes, it works perfectly fine, but with two main caveats:
1. It is single user, single connection (i.e. no MVCC)
2. It doesn't support all postgres extensions (particularly postGIS), though it does support pgvector
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.
2. If you change your handle (for did:plc, did:web can't do this because DNS) it used to break links but nowadays this isn't a problem because handle resolution respects historical handle naming (I think it works by post+handle age but I can't remember).
3. Also if you share posts using the did syntax instead of handle syntax (which bluesky seems to be slowly changing over to, at least profiles do this now), it's stable regardless of handle changes.
4. If you want to switch frontends, you can use an extension or app like at://wormhole to do so. UX for this should improve over time but that's a big "eventually".
5. Hopefully the at:// URI format catches on but that's a long ways away given that browsers make using custom URIs an absolute nightmare.
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.
MOOCs are still going strong at India's NPTEL , which started distributing university-level video courses for engg in 2008:
- 5m subscribers, almost 2B views on youtube
- 30m enrollments
- 600+ courses every semester in 22 disciplines
Anyone from the world can signup. Proctored exams are optional and cost about $11 per course. Not taking VC funding and setting up local chapters for supporting students seems to have worked out well for them.
Seems that Google intend it to be that way - https://ai.google.dev/gemma/docs/capabilities/function-calli... . I suppose they are saying that the model is good enough that if you put the tool call format in prompt it should be able to handle any formats.
I use PetrosStav/gemma3-tools and it seems that it only works half of the time - the rest the model call the tool but it doesn't get properly parsed by Ollama.
unfortunately, I don't think gemma 3 supports tool calling well. It's not trained into the model, and the 'support' for tool calling is post model training.
We are working with Google, and trying to give the feedback on improving tool calling capabilities for future Gemma models. Fingers crossed!
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.
Why can't we just prove theorems about the standard two's complement integers, instead of Nat?
reply