โ„๏ธ๐ŸฆŠ is a user on octodon.social. You can follow them or interact with them if you have an account anywhere in the fediverse. If you don't, you can sign up here.

Me:

I want all my code to be able to do anything to anything on my computer, no questions asked.

Also me:

I want to take code from anywhere and run it just like my code so it can do anything to anything.

Also me:

I want the code I run from anywhere that can do anything to anything to NOT actually do anything to anything UNLESS I want it to do that.

Also me:

I don't know precisely what 'want' means and I don't want to have to check every piece of code myself to see if I want it to do stuff

@natecull so...

You want an operating system, and a method of dealing with other operating systems that have different assumptions.

With proofs attached. That are composable and amenable to inference.

I'm honestly sure we'll get there someday but it will be a long fight.

@icefox well, I'd settle for 'just one language with this property'

problem is I don't quite know what that property *is*

@natecull the problem is abstraction.

Operating systems are an abstraction of the hardware. It, on *some* level, doesn't matter whether you are running on x86_64 with "PC" hardware or on PPC with "Mac" hardware or on ARM with "cell phone" hardware

But when you go deep enough it *really* matters

And those abstractions have costs and hunams want to minimize those costs so pure abstractions are very problematic.

@natecull And when you go deep enough in those abstractions you come down to something like a Turing machine and so the math all works but the intermediate layers are all really problematic so you can't pretend they don't exist. So you get engineers searching for the least problematic perspective.

You know all this, cat. I'm just rambling.

@icefox I really hate the Turing Machine. One giant memory space that any cell can overwrite? Really?

I know it works for doing maths but it's.... not the best design for security.

@natecull pfft come now

In principle, process isolation is just a projection. (As far as I can tell.)

I can't help if the RL implementations suck.

@icefox I wonder if the TM could be rewritten as 'get data from' rather than 'write data to' rules, and if that would help

(that's basically what functional programming is, I guess? but I still struggle to understand how FP can deal with mutation in finite resource spaces)

โ„๏ธ๐ŸฆŠ @icefox

@natecull maybe. Lambda calculus is a nice solution. You can basically prove that your stuff works and also that certain parts of your state are irrelevant (ie can be garbage collected) so the finite-ness is less of a problem.

ยท Web ยท 0 ยท 1

@icefox yeah, I guess LC is a 'pull' form where TM is a 'push'. But dealing with time-changing large structured data is still hard.

eg: 'The telephone book has a bunch of new names in it, but I don't want to have to download the whole thing, BUT I also want to be able to search fast so I need it to be sorted and in one place'

@natecull Yeah it's tricky, afaict. (I'm not a mathematician. Ping @Azure or @dasyatidprime for real rigor rather than vague intuition.)

Real time-change data is Hard to deal with in a representation that isn't O(n) with time in space and O(n^2) with time in complexity, I suppose. The person who finds out how to deal with that nicely go down in history with Euler.