the point I like Alloy is that it allows you to express something like "forall function f such that f is well-define ...", very cool. I barely know anything ab

the point I like Alloy is that it allows you to express something like "forall function f such that f is well-define ...", very cool. I barely know anything about TLA+ though.