The real question is: for a typical program we prove it - even though we know there are programs we can't prove?

I don't care about the examples given, I care about my word processor, web browser and such. Can we prove them - putting limits on the scripting language

▲

mrkeen 2 hours ago | parent | next [-]

It's certainly not the whole story, but I haven't seen a better vehicle for trustworthy code than pure functions.

I might want my code to dabble in CORS, read env vars, or snoop around in my .ssh directory, but I don't want my imports to be able to do that.

	▲	aleph_minus_one 2 hours ago \| parent [-]
		> I might want my code to dabble in CORS, read env vars, or snoop around in my .ssh directory, but I don't want my imports to be able to do that. OpenBSD has a (partial?) solution for that: pledge (2) https://man.openbsd.org/OpenBSD-6.7/pledge.2 Often, a programming needs a lot of rights at the start to set things up (often even root permissions). After this has been done, it should better have irrevocable limited rights. The pledge() syscall is there to do this transition: "Subsequent calls to pledge() can reduce the abilities further, but abilities can never be regained."

▲

aleph_minus_one 2 hours ago | parent | prev [-]

> putting limits on the scripting language

Putting limits on a scripting language should not be too hard (even without talking about any correctness proof). And I would bet that for a scripting language where the limits are in a way that "in a correct implementation, it should be highly likely that these limits are actually enforced" (i.e. the specification of the scripting language has no parts that makes you suspicious whether there exists some loophole that a malicious actor could use to overstep the limits), it should actually be possible to write a verified implementation with some effort.

But this is not what people want: for example, basically every evolution of the web standards since HTML5 by the WHATWG was about extending what is possible to do in the scripting language (JavaScript).