Porffor: A from-scratch ahead-of-time JS engine

Re:Porffor: A from-scratch ahead-of-time JS engine by mike_hearn on Wednesday July 31, 2024 @04:29AM (#41117348)

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.

[ Parent | on HN ]

Re:Porffor: A from-scratch ahead-of-time JS engine by g15jv2dp on Wednesday July 31, 2024 @05:35AM (#41117628)

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?

[ Parent | on HN ]

Re:Porffor: A from-scratch ahead-of-time JS engine by mike_hearn on Wednesday July 31, 2024 @07:47AM (#41118319)

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.

[ Parent | on HN ]

Re:Porffor: A from-scratch ahead-of-time JS engine by skitter on Wednesday July 31, 2024 @10:13AM (#41119345)

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.

[ Parent | on HN ]