Без заголовка

Статическая или динамическая типизация тут не имеет значения, это в бОльшей мере инженерный, а не научный вопрос: просто для динамических языков проверка делается в ходе выполнения программы, а не перед выполнением, в обмен на гибкость мы получаем более медленное исполнение. Вообще говоря имеет, ибо при динамической типизации верификатор сам должен догадываться, какие типы может принимать выражение. Так что символическое исполнение тоже будет более медленным. И что более важно, оно будет автоматически разрешимым в меньшем кол-ве случаев.