3 ms·
The problem with your analogy is that C and Java have completely different abstract syntaxes. A better analogy would be taking the syntax of an existing program
by catnaroek 11y ago
The problem with your analogy is that C and Java have completely different abstract syntaxes. A better analogy would be taking the syntax of an existing programming language, and completely changing its meaning. For instance, consider the effect of making Racket use lazy evaluation (Lazy Racket), or making Haskell use strict evaluation (the upcoming -XStrict pragma). Strict and lazy languages validate different sets of equational laws (and hence compiler optimizations!), neither of which is a subset of the other, so this is perhaps a more interesting example than switching between intuitionistic and classical logic.
- plutooo 11y agoBut I'm saying if you evaluate the axiom symbols two different ways, it's two different axioms.
- catnaroek 11y agoWhat you're saying is more or less equivalent to “two C implementations targeting different [architectures / operating systems / whatever] are actually implementations of two different programming languages”.
- plutooo 11y agoNo, I'm saying the meaning behind statements are different. On some architectures, an int is 16-bit, on others 32-bit. Anyway, this analogy was pushed too far a long time ago.
- catnaroek 11y agoAh, lovely! You just arrived exactly where I was trying to get. > I'm saying the meaning behind statements are different. Yes, exactly! And, just like a single C program can have two different meanings under two different implementations, the same axiomatic system can have two different meanings when deducing its consequences (proving theorems) using different rules of inference.