3 ms·

This is specifically about type systems. It's easy to have a sound type system when you have no type system. Also, I'm not too familiar with JVM bytecode, but

This is specifically about type systems. It's easy to have a sound type system when you have no type system. Also, I'm not too familiar with JVM bytecode, but if I load i64 in two registers and then perform floating point addition on these registers, does the type system prevent me from compiling/executing the program? Can you say more about "proven to be sound"? Are you talking about a sound type system?

mike_hearn 2y ago
It does have a type system. https://docs.oracle.com/javase/specs/jvms/se22/html/jvms-2.html#jvms-2.2 https://docs.oracle.com/javase/specs/jvms/se22/html/jvms-2.h... JVM is a stack not register machine and yes the type system will prevent that from running. It will fail verification.
skitter 2y ago
The type checker is specified in Prolog and rejects the above scenario: instructionIsTypeSafe(fadd, Environment, _Offset, NextStackFrame, ExceptionStackFrame) :- validTypeTransition(Environment, [float, float], float, StackFrame, NextStackFrame), exceptionStackFrame(StackFrame, ExceptionStackFrame). Fun fact: Said type system has a 'top' type that is both the top type of the type system as well as the top half of a long or double, as those two actually take two values while everything else, including references, is only one value. Made some sense when everything was 32 bit, less so today.