If we program by conjuring spirits

Where in the CPU the spirit is located?

In the magic smoke, duh.

http://medium.com/tag/perl/latest

>>1
"If a subsystem is Turing complete, than so too is the Whole." - Ancient /prog/ koan, for your contemplation.

The spirits are encompassed within the CPU, the memory and mobo bus lines.

So I've been thinking about the testing vs program verification (type safety etc), how testing can never prove the absence of errors etc. I think these academics are missin out one key point: there is only a finite set of programs that solve a particular problem and don't have superfluous stuff and don't look like gibberish. Right? And with every test you perform, you're narrowing down the space of those programs, and it's possible to arrive with testing at the one unique (up to some equivalence like reordering some shit) program that is correct.
On the other hand, type systems and program verification can not really prove the absence of errors either. They only prove what you've had the ingenuity to prove and encode in the type system. Simple example: you're writing a financial accounting program and you've used floating point numbers. Will it typecheck? Yes. Will it behave erroneously? Yes, because you forgot that your AccountSum type must have integer representation, and didn't encode that into the type. The type checker is never smarter than the programmer, it's just more diligent and thorough, that's all.
So what I'm getting at here is that testing and program verification are really two different approaches to program correctness and none of them is better or worse than each other. There are cases where testing will cover your ass while Coq won't, and vice versa. So you academics can't really be looking down on us all with your type theory an shit. And there are reasons why dependent types aren't picking up, cause they might be too little bang for the buck and still not 100% guarantee your programs are correct.

>>6
But if your language is absolutely untyped, you also need to test your code passing objects/strings/etc as input data, or make sure it is impossible (write type checks throwing errors in each function).
So, type checking is limiting the amount of tests you need to write.

>>6
program verification is not just typechecking though. you can formally verify whether program has rounding errors or not. you are right though - the current state of things makes testing more practical than formal verification.

>>7
Sure, testing and type safety have an overlap, but none of them subsumes another. The type system may check that you don't pass a number instead of string, but will it check that the string is non-empty or the number is non-zero or the email string contains exactly one '@' symbol? You still would need tests for it, or dependent types. And the guarantees of both still depend on the programmer. Did you remember to test for the one '@' per email rule? Did you remember to encode that rule in your dependent type? Either way you don't get automatic guarantees.

>>8
Yeah there's Ada SPARK. Don't know which is more painful to use, that or dependent types.

>>5
Are you certain, dear friend? If one takes a moment to fully reflect upon the essence of >>4, it should begin to dawn upon your mind and imprint itself into the very core of your being that the CPU is far more than the extravagant constellation of particles, atomic and sub-atomic, that first meet the eye. No, it is the elegant configuration of these particles that is far more important, for it is what makes the whole greater than the sum of its parts.

Analyzing the spectral decomposition of the quantum amplitude phase-spaces and configuration-spaces of these subsystems and cross-sections of particles that embody the CPU, one discovers a taxonomy of unique causality and homeodynamic constraint classes. When these constraints are superimposed upon one another in the very precise manner alluded to, they allow for the emergence of higher-order contragrade (entropy reducing) processes that produce useful activity from the lower-order orthograde processes (entropy producing). In effect, a CPU may produce interesting and meaningful (teleodynamic) work as a consequence of it being constructed of physical and abstract things that possess particular information constraints and of it exploiting latent entropic forces, both of which preexist, are a part of and underly the cosmos as a whole. The same cosmos--the same reality in which both you, me and the CPU are but an insignificantly tiny subset. Church–Turing–Deutsch Principle. All physical processes are computable and a universal computing device can simulate all physical processes. Hence, if the entire cosmos is computable, it follows that there is one computational spirit that permeates all things. Furthermore, if a subset (CPU) of a system is Turing complete, then it is trivially true that the entire set (cosmos) is also Turing complete. Quod erat demonstrandum.

The CPU is the spirit, the ghost is the machine. The All is data, everything bits. META-CIRCULAR EVALUATION OF YOUR SOUL. λδ -- την απόλυτη. The sublime serenity and abstract horror of our existence.

https://p.fuwafuwa.moe/nfgyur.webm

>>10
You're junk Suigin, but we all love you! I hope you get to feeling better about yourself and your injuries heal :3.