Very interesting, thanks (and to the other sibling poster).
> Tom's TLA+ version was closing in on 200 pages, available at [snip]
This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking by computer-based proof assistants, but I digress...
One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.)
Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?
> Tom's TLA+ version was closing in on 200 pages, available at [snip]
This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking by computer-based proof assistants, but I digress...
One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.)
Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?
EDIT: Russel & Whitehead