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.

@MatejLach @Wolf480pl @cbowdon

Also why build a state of the art shit whose shape has beed already defined by #Google instead of building something new and better?

Something following a totally different vision?

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

I think we need a #CERN of #Informatics, but it should start from a simple vision and build what it takes to get there from the ground up.

I have a vision to propose: all people should be able to read, understand and modify each software they use or feed with their data.

Modern Web is not going to survive such vision, so building a browser is wasting money imho.

@MatejLach @Wolf480pl @cbowdon

@alcinnz @z428 @MatejLach @Wolf480pl @cbowdon

Guys, that's just because we are at the hieroglyphs of #Informatics.

If it's difficult to explain it's because it's primitive. Let's invent the right alphabet and every kid will be able to learn programming at the primary school.

@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

Imagine a wonderful future where spreadsheet like #UI is #homoiconic to a strongly typed #Lisp that is based on #Cantor set theory.

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

Eww.... set theory? ugly!

Follow

@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.

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

Mind to describe a computation you couldn't describe with Cantor's sets?

(all I know about type theory, I've learnt from Haskell documentation and a few other casual readings... be patient...)

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

This is what I have in mind: https://mastodon.social/web/statuses/101477076992077093

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

(roughly: actually that's not a specification, but a description typed at the smartphone ðŸ¤£ )

By constructive sets I mean sets that can only be defined either as subset of other sets or by products of other sets with few base set that are Empty, Truth, Naturals, Functions, Products (aka tuples) and Sets.

Note how the Sets set is not an element of itself. ðŸ˜‹

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

Can I have a set of functions?

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

Why not?

It would be pretty useless in itself as an un-castable array of (void*) but you could construct it by such definition.

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

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

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

You could, but you could not invoke any of such functions (there is no way to cast) so I'm not much sure what you mean... (but I'm eager to understand if you mind explaining)

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

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

Uhm... yes you said "a set of all sets". But it's just as useful.

I'm missing something obvious?

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

it contains itself...

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

not anymore?

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

Uhm... the Sets set is a set but since all sets can only be defined in terms of the existing base sets (as either subset or products OR UNIONS, sorry forgot to mention that) and it is a distinct basic set whose element are automatically assigned by the compiler...

@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?

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

Uhm... so the problem with set theory is that it's too powerful for a computer?

Shouldn't this be something to ask a computer? ðŸ¤£

Jokes apart, ultimately you are saying that there's no way to know with set theory if the complier will ever finish the computation?

I look at the problem from a different angle: whatever you can do with a typeclass you can do by explicitly passing a tuple of functions for each typeclass as a function arg.

Rain ðŸš±@grainloom@cybre.space@Shamar @Wolf480pl @z428 @alcinnz @MatejLach @cbowdon If you can only prove that something exists but can't construct it... how is that going to translate into useful computation?