I agree that the verifier performance is not important to runtime performance (though there have been some changes to the JVM in particular to speed up class loading), but the expressivity of the safety proofs it can check is, because safety properties that cannot be proven at load time must be checked at runtime. Initially, and I think still, the JVM's downcast on loading an object reference from a generic container like ArrayList<Price> is an example: javac has proven statically that it is safe, but the JVM bytecode cannot express that. Pointer nullability in JVM languages like Kotlin is another example: Kotlin knows most object pointers can't be null, but the JVM still has to check at runtime.

There have been numerous holes discovered in various implementations of the basic JVM type checking, often after existing for many years.

▲

pizlonator 5 days ago | parent | next [-]

The JVM byte code situation isn’t a great example because that was a series of deliberate design choices for lots of complex reasons. And, the JVM absolutely can guarantee memory safety at the bytecode level. It’s just working with a slightly more dynamic type system than Java source.

What would happen if you tried to do PCC for InvisiCaps and FUGC is that it would ultimately constrain what optimizations are possible, because the optimizer would only be able to pick from the set of tricks that it could express a proof for within whatever proof system we picked

Totally not the end of the world.

Do I think this an interesting thing to actually do? I’m not sure. It’s certainly not the most interesting thing to do with Fil-C right now

	▲	kragen 4 days ago \| parent [-]
		Yes, I agree with you that a correct JVM can guarantee memory safety at the bytecode level, but what I meant to express was that many JVMs have had bugs that caused them to fail to do so, for essentially social reasons which I expect to cause problems with other PCC systems as well. Maybe you're right, and those problems are not inevitable; for example, if you could reduce the proofs to a tiny MetaMath-like kernel that wouldn't need constant "maintenance". As you say, that could move the compiler's optimizer out of the TCB — at least for the security properties Fil-C is enforcing, though the optimizer could still cause code to compute the wrong answers. That seems like something people would want if they were already living in a world where the state of computer security was much better than it is now.

▲

gf000 5 days ago | parent | prev [-]

I mean, since Gödel we pretty much have known that there could never be a system "without holes".

▲

kragen 5 days ago | parent [-]

No, that is not correct. Gödel showed that some theorems are unprovable in a consistent formal axiomatic system; he did not show that no consistent formal axiomatic systems exist.

▲

gf000 5 days ago | parent | next [-]

He did show that every formal axiomatic system will have statements that can't be proven "from within".

For these, you are left with doing a runtime check.

	▲	kragen 4 days ago \| parent [-]
		Yes, that's true, but then possibly we are talking at cross-purposes; when I said "numerous holes discovered in various implementations of the basic JVM type checking", I didn't mean things that needed to be checked at runtime; I meant bugs that permitted violations of the JVM's security guarantees. However difficult it may be to avoid such things at a social level, certainly there is no mathematical reason that they must happen.

▲

naasking 5 days ago | parent | prev [-]

> Gödel showed that some theorems are unprovable in a consistent formal axiomatic system...

...of sufficient power, eg. that can model arithmetic with both addition and multiplication. I think the caveats are important because systems that can't fully model arithmetic are often still quite useful!

▲

gf000 5 days ago | parent [-]

Indeed! But I am afraid general purpose programming languages almost always need that kind of power (though being Turing complete is not necessary)

	▲	naasking 11 hours ago \| parent [-]
		They need it operationally for calculations and such, but those calculations don't necessarily need to be statically validated beyond simple things like type and unit checking.