is cyp's work (polynomially, linearly) bounded?

[jwaldmann]

As I'm planning to use this in an online system: could this be DoS-ed?
Are there short proofs where checking would be expensive?

But the proof language is rather explicit - so cyp never has to guess/search? Well, it guesses the subterm where a rule is applied, and the direction of the rule application. But the work is still linear in the size of the term, and the term is written in the proof.

What else could go wrong? Like, too much backtracking in the parser, or even: inefficient pretty-printing ( haskell/pretty#32 )

If we do type-inference, then that's another surface for attack (naive unification algorithms, or naive printing of inferred types in error messages)

(I do have other safety measures in place already.)