**Nate Cull** @natecull@mastodon.social · May 10, 2018, 00:15

**Nate Cull** @natecull@mastodon.social · May 10, 2018, 00:15

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

**❄️🦊** @icefox@octodon.social · May 10, 2018, 00:21

**❄️🦊** @icefox@octodon.social · May 10, 2018, 00:21

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.

**Nate Cull** @natecull@mastodon.social · May 10, 2018, 00:24

**Nate Cull** @natecull@mastodon.social · May 10, 2018, 00:24

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

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

**Adrian Cochrane** @alcinnz · 2018-05-10T00:59:11Z

Adrian Cochrane @alcinnz

@natecull @icefox Victoria University's David Pearce is working on a language with proofs you might be interested in, Whiley.