Hacker News Reader

Comment by mike_hearn | Hacker News Reader

JVM bytecode is a "language" and is proven to be sound. The languages that compile to that language, on the other hand, are a different kettle of fish.

View on HN

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?

It does have a type system.

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.

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.

Reply on news.ycombinator.com