> It emerges from the underlying mathematics.
Which mathematics?
(Lisp has its own math, for instance.)
Which mathematics?
(Lisp has its own math, for instance.)
I agree there are correctness properties we can prove without running a 'program', but how do we map the notion of a 'program' into the real world. Is a single function a program? A single module which includes multiple functions? A single executable? A single system that includes multiple processes communicating over a network? I'm arguing each of these is a 'program' and a Turing machine in the theoretical sense. Each of these programs is hooked up to other 'programs' outside of it. 'Compilation' requires the input to be static, but if we think about how things are in flux (you can change a function, switch out a shared library or upgrade and restart a running process, etc.) when do you verify that a 'program' is 'correct'?
This is what I mean by 'compile time is made-up' - it falls out of the current frame of thinking of one OS process = one program = static set of source files. It is possible to design systems that have no notion of 'compile time'. You could still have verification, but it could be incremental and spread out all through the lifetime of the running system. So the system would have no 'compile phase' - it would be running live and as you update parts of it, the updated parts would integrate with the rest of the system and do verification like things.
> The internet is dynamically typed.
That's an incoherent claim.
Dynamic typing is where types belong to values. Static typing is where they apply to terms.
Really to call the former "typing" is misnomer. It's an abuse of the word "type" to mean "memory mode". It has not much relationship to typing in the logic/math/philosophy of logic sense in which types are sets and type relationships are those between sets.
It is the Curry-Howard isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) which defines the correspondance between types in computer science and mathematics.
This is "static" only because the "dynamic" alternative isnt really an alternative at all, and really just a different kind of thing all together.
The claim is logically incoherent: typing cannot be a property of the internet, in the same way tuesday cannot be pink nor can addition sound terrifying.
The claim is a category error: the internet cannot posses such a property.
In addition, to say, of something, that it is " is a made up thing " is a degree of hubris that is presumably reasonably met by being perplexed at overconfidence of the claim posed with such little correct information.
Is being perplexed more uncivil than hubris? Are we really policing people's language to this minute degree?
Actually you broke this guideline as well: "Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize." It's possible that shalabhc intended to make a mathematical claim, but a stronger plausible interpretation is easy to come up with (e.g. "it's hard to enforce static guarantees across the software that interoperates on the internet").
The reason we ask people to follow this guideline is not so much that it's nicer, but that nitpicking things each other probably didn't say is tedious and detracts from good conversation, which is what we're really hoping for.