А вдруг кто-то может подсказать, насколько реально, например, иметь Zero в качестве интерпретатора и вместо Shark прикрутить к нему C1/C2 или J9(предположим, они спортированы) вместо стандартного(?) в этом случае Shark?
Если я правильно понимаю, то принципиально интерфейсы jit'ов к рантайму не то, чтобы сильно различаются, но это я еще буду внимательнее смотреть

Я тоже

Я ошибаюсь или она никогда и не была частью стандарта?

Оракл паковало в свою ждк, но в опенждк в поставке же javafx никогда не шёл

Ну она есть например в зулу если я не ошибаюсь

Да, вижу заанонсили в декабре что будут бандлить со своей Zulu jdk8 и дальше

оффтопный вопрос, простите меня

Грааль же вроде детище оракл лабс, если не путаю. И говорят что в оракл лабс пользуются для чего то формальной верификацией. Может что-то слышали и можете рассказать для чего именно?

GraalVM пожалуста

не, не знаю, могу спросить у кого-нибудь, у вас есть поточнее формулировка вопроса?

ищу кейсы практического применения формальной верификации в жизни и в одном чате упомянули оракл лабс (без деталей совсем)

ага, сорри, я не знаю

жаль
ну лан, не буду больше оффтопить

Формальную верификацию часто применяют при разработке железа.
ну а мы, например, формально верифицировали скедулер в собственной операционке

Байткод верифицируется перед исполнением, а что конкретно "формально верифицировать" можно в компиляторе?

например, rewriting rules

систему типов

что оптимизации корректные

Проход по графу промежуточного представления после каждой оптимизации - формально является верификацией. Но это построенная SSA гарантирует, а вот то что обращения в память не поменялись для конкретного бенча - это как-нибудь проверяется?

Граф он у конкретной программы, его обход фактически вычисление.

То как мы можем изменить граф в другой, задается набором каких-то операций (например deforestation в хацкелле). Они не зависят от конкретной программы и могут быть применены в каждой (потенциально). Поэтому хорошо бы доказать, что эти правила не меняют результата. Вот их к примеру и можно описывать формально и доказывать (на бумажке или пруверами).

Немного политики в ленту