A modern programming language that makes developers happier.

kotlinlang

I am curious if type-proofs and arrow-meta have proven to get around some of the expensive boxing that the jvm normally imposes

They help removing virtual dispatch since you can project syntax from a type to other without interfaces or abstract classes just through a function

Also specially when proofs are declared inline

For the rest I'm not sure we can do more than what inline classes do.

We plan on investigating a form of polymorphism based on top level functions where implementors are inlined and abstract functions can be used as templates. That could remove indirection through interfaces.

That is specialized implementors to data types to remove polymorphism and using just abstract functions as inline templates

Still to be researched and in idea stage. We did a small prototype but left it because it required more time