数学者だって、自分の専門分野の数学をすべて論理学と集合論の公理から演繹したわけじゃないだろう
すでに理解したことやよく知られた事実は認めて問題を解いているはずだ

そういう柔軟性がほしい
つまり、認めてもいい仮説はその場その場で手軽に導入できるような言語設計がいい
その上で、そこから機械的に導けることの証明や、定義から直接わかる具体例の計算などを半自動でしてほしい

もちろん、コンピュータにやらせる以上、曖昧さのない構文は必要だろうが

def continuous_at(f: Real -> Real, a: Dom(f)) = forall({e: Real | e > 0},
exists({d: Real | d > 0},
forall({x: Dom(f)},
implies(abs(x - a) < d, abs(f(x) - f(a)) < e)
)
)
)

これよりもさらに手短に、見た目ももっと見易く