В смысле - меня попросили посмотреть и по возможности поломать ее верификатор (ради которого она собственно и существует).
Системка по задумке интересная - предназначена для доказательства функциональной эквивалентности разных функций на C, Java и Cryptol* (вещь на сам деле нужная очень - потому ситуация когда есть неэффективная но простая референтная реализация и ее эффективный но совершенно нечитабельный "прикладной" вариант довольно обычна и ловить там баги на расхождениях - удовольствие то еще), ну и на сам деле и несколько более сложных вещей (возможно отпишусь подробнее отдельным постом) и на приведенных в поставке примерах (весьма нетривиальных) демонстрирует вроде бы круть немерянную.
Нужно было собственно резюме как к ней следует относиться при обсуждениях всяких смежных тем. Ну обычное в таких ситуациях - на вопрос "а что вы думаете вот про это?" желательно иметь разумный ответ.
Результат оказался впечатляющим - из трех тривиальнейших примеров (все три намного проще ихних) на двух с половиной до собственно верификации дело не дошло - в первом случае функции в одну строчку отработали с аргументами типов int8_t и int16_t, а на (вообще-от естественном как раз) int32_t система сказала ква - судя по всему криво оттраслировав код в Сryptol-based IL - сломалось на проверке типов (там даже примерно понятно в чем лажа).
Остальные два - фиббоначи (рекурсией и циклом) и факториал - циклами "туда" (от 0 до n) и "обратно" (от n до 0) закончились зацикливанием импортера llvm-ного кода. Причем второй - на варианте "туда" ("обратно" как раз загрузился нормально). Первый зациклился на рекурсии.
С жабой тоже самое впрочем.
Потому и возник собственно вопрос - "а как они этим вообще пользуются"
*) Собственно SAW и есть добавка к Cryptol и активно его пользует унутре скриптов - главная идея как я понимаю писать алгоритмы на криптоле и доказывать что их С- и Java- аналоги им эквивалентны