alt Hacker NewsThe 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
Replies
> 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).
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.