Думаю, что в этом форуме обитает народ занимающийся theorem prover-ами и прочими логическими штуковинми.

Вопрос к ним...

Можно ли использовать Z3 theorem prover (видео по его кострэйн-солверу) для вывода типов в языке вроде Nemerle?

Посню в чем собственно сложность в выводе типов.

Основных проблемы...
1. В системе типов имеется наследование (subtyping).
2. Присутсвтует явное и не явно (в том числе определяемое пользователем) приведение типов.
3. Присуствуют перегрузки.

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

Сейчас используется следующий алгоритм решения этой задачи.

При типизации выражений внутри отдельного метода строится граф типов. Для построения и проверки графа используется кострэйн-солвер написанный Москалем еще в бытность учебы в универе. Далее создаются объекты отложенной типизации которые могут содержать недотипизированные части АСТ и такие гипотетические ветви типизации применяющие разные вариант перегруженных методов. Далее начинается последовательные попытки стипизировать все возможные сочетания перегруженных методов, приведений типов и уточнений типов.

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

Проблемами текущего алгоритма являются:
1. Серьезные тормоза вызванные огромным числом переборов и тем что постоянно требуется откатывать состояние солвера (при спекулятивных типизациях).
2. Сам процесс получается, скажем так, "императивным" в том смысле, что вместо построения некой модели всего кода метода и ее проверки мы вынуждены искать путь путем проб и ошибок. Попробовали стипизировать так — не получилось, попробовали иначе — получилось... поехали дальше... Фактически наличие вложенных вызовов и большого количества перегрузок (что характерно, скажем для линка) приводит к тому, что одно тело метода может типизироваться 1-3 секунды (на современном процессоре).
3. Иногда шаги типизации дублируются. Один и тот же алгоритм может выполняться при прямой типизации и при отложенной.

Хотелось бы как-то ускорить этот процесс и сделать его более структурированным.

В идеале хотелось бы построить что-то вроде модели кода метода содержащей в отдельных АСТ-ветках некое дерево возможных вариантов типизации (например, для разных перегрузок метода), скормить эту модель некому "думателю" и получить модель дерево в котором остались только корректные подветки.

Правильно ли я понимаю, что Z3 как раз то что нам нужно?
И возможно ли вообще (на современном этапе развития науки) то что я описал?