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.

@MatejLach But how would you unseat Chrome at this point? Google have the incumbent advantage and the platform advantage. Technical excellence is only part of the story.

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

@MatejLach Ooh that last one is a good one. That’s what MS/Apple/Google are trying after all. You wouldn’t necessarily need CERN-like levels of funding to achieve it.

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

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

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

@Wolf480pl @cbowdon

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

@Shamar@mastodon social It won't work. Just take some time to, say, explain recursion or graph algorithms, image compression or even cryptography math to a totally untrained user. We will never get to a point of end users to read or understand their software. IMHO, trying to do so is a waste of time that could better be spent on building more ethical solutions that just work for this crowd.
@MatejLach @Wolf480pl @cbowdon

@z428 @MatejLach @Wolf480pl @cbowdon My position is that they should be *able* to (perhaps with a little training), but not obligated to.

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

@Shamar We're at a point where some adults have issues understanding higher math, some even have real issues learning to master natural language to understand complex texts or express themselves. And we actually did invent an alphabet to help these folks: Icons. Symbols. Easy interactions. So far this works well. Will we be able to do meaningful programming on that level?
@alcinnz @MatejLach @Wolf480pl @cbowdon

@z428 @Shamar @alcinnz @MatejLach @Wolf480pl @cbowdon in simpler systems, the meaning of "meaningful programming" might be a lot different than it is in bloated corporate software. just want to get that noted.

@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 :blobsurprised:

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

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

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.

· brutaldon · 1 · 0 · 1

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

@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

(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. 😋

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

@Shamar @grainloom @z428 @alcinnz @MatejLach @cbowdon
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)

@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

@Shamar @Wolf480pl @z428 @alcinnz @MatejLach @cbowdon It's not that you can't describe but that not everything you can describe can be computed. Eg.: existence proofs by contradiction.
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.

Sign in to participate in the conversation
Cybrespace

Cybrespace is an instance of Mastodon, a social network based on open web protocols and free, open-source software. It is decentralized like e-mail.