Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements). I once wrote a pretty disgusting Java-implementation

Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements). I once wrote a pretty disgusting Java-implementation of that concept. And if you didn't use the stdlib, nulls and who knows what else and you managed to return the type only using your input parameters (that is, you had your function signature as the statement you want proven and the body was your proof of that), then your statement was "proven" to be true.