We need a multi-national, publicly funded research organization akin to CERN/within CERN, whose whole purpose is to develop a state-of-the-art browser that's not Chromium-based. Make #Google follow our lead, rather than us having to follow Google.

If the Web could be developed using public money, why not a modern browser? Public funding would remove the Mozilla problem of them having to depend on Google.

With the amount of money governments waste annually, we could fund this AND Mozilla.

There could be incentive problems here as well, of course, like governments threatening to withdraw funding in case a certain backdoor isn't included, or if it blocks ads too aggressively and some corporate-funded 'representative' starts receiving pushback from the industry etc, but which is why it would need to:

- Be funded by a wider variety of states than the Five/Nine Eyes members.

- Developed entirely in the open, each important change reviewed by a committee of experts from the public.

@cbowdon That's definitely going to be a challenge, but #Google did some smart marketing by having ads IRL, like in trains and such, even in smaller countries if the % of connected users was high enough.

Since it would be publicly funded, you could also install it on computers in publicly-funded educational institutions. A lot of software spreads by children installing it for their parents. If students are using it at school, they're likely to install it at home.

but wouldn't you need CERN-like levels of fuding to develop a browser that keeps up with the moving target of shitty WHATWG standards?

@Wolf480pl

That was indeed my thinking as well.

I think to pull regular users in, we'd have to start with today's web. But once we have sway in the committees, you can begin to redefine what state of the art web should look like.

@MatejLach @Wolf480pl @cbowdon

@alcinnz @MatejLach @Wolf480pl @cbowdon

@grainloom @z428 @Shamar @alcinnz @MatejLach @cbowdon

Btw. notice how the alphabet that supplanted the hieroglyphs was Phoenician alphabet - one that was used by merchants.

Now what do merchants use these days to do programming.... spreadsheets.

How hard is it to teach a 7yo how to use spreadsheets?

@grainloom @z428 @Shamar @alcinnz @MatejLach @cbowdon

OTOH, imagine this wonderful future, where spreadsheets are the new JS and everything is even slower

@Wolf480pl @grainloom @z428 @alcinnz @MatejLach @cbowdon

Type theory was invented to address paradox in Cantor set theory that he dismissed with something like "these dudes didn't do their homeworks".

What if ultimately he was right? ;-)

Would it be the first (or the last) time where people built overcomplicated systems and notation because it was more appealing than the simplest possible solution?

@Shamar @grainloom @z428 @alcinnz @MatejLach @cbowdon

Can I have a set of functions?

Can I have a set of functions whose return value is a boolean?

If so, I just made a set of all sets.

I just defined a set of all sets, what more to you need?

@Shamar @grainloom @z428 @alcinnz @MatejLach @cbowdon

it contains itself...

>Note how the Sets set is not an element of itself.

not anymore?

@Shamar @Wolf480pl @z428 @alcinnz @MatejLach @cbowdon fric, my folder with all the cool papers is empty and I can't find the url for it but uuh there is existing research for doing namespaces and stuff like that...

uuuh @abs what was that very cool thingy you sent me??

@Shamar @Wolf480pl @z428 @alcinnz @MatejLach @cbowdon

anyways, you don't need to base the language on set theory but you could use set theoretic notions to describe key-value pairs and that can be used to implement namespaces and structs

this is super nice because it'd be a bit like Lua's module system, where modules are really just tables

@grainloom @alcinnz @z428 @cbowdon @MatejLach @Wolf480pl @Shamar I think this is it: https://web.cecs.pdx.edu/~mpj/pubs/96-3.pdf

Not 100% certain, though.

Not 100% certain, though.

@abs @Shamar @Wolf480pl @MatejLach @cbowdon @z428 @alcinnz Thanks, that seems to be it!

But afaik you can express the useful parts of set theory in type theory, so why not just go with type theory?

Rain 🚱@grainloom@cybre.space@Shamar @Wolf480pl @z428 @alcinnz @MatejLach @cbowdon The main thing I like about type theory is that all your proofs are constructive. You don't get that in set theory.

Also set theory is not good for automatic proof checking.