Здравствуйте, Трурль, Вы писали:

Т>Здравствуйте, GlebZ, Вы писали:

1>>>а может можно придумать высокоуровневый язык для описания доказательств теорем и вообще любых математических утверждений?
GZ>>И назовем его SML!!!! (или кто-то уже делал такой?)

Т>SML — не для "описания доказательств теорем", а для "программироваия систем доказательств".
Собственно HOL и Coq , ровно также как и LCF (ради которого был создан ML) ---- написаны на ML.
не думаю что это будет верх эволюции.