How can we make neutrinos useful to us? - https://www.youtube.com/watch?v=F0HQp2nBFhI
What are neutrinos good for? - https://www.youtube.com/watch?v=-6iyyM5XRx4
5,890 karma · joined December 4, 2018
===== The Problem: Realism vs. Idealism =====
“Do you know, I sometimes catch myself wishing that I, too, were blind to the facts of life and only knew its fancies and illusions. They’re wrong, all wrong, of course, and contrary to reason; but in the face of them my reason tells me, wrong and most wrong, that to dream and live illusions gives greater delight. And after all, delight is the wage for living. Without delight, living is a worthless act. To labour at living and be unpaid is worse than to be dead. He who delights the most lives the most, and your dreams and unrealities are less disturbing to you and more gratifying than are my facts to me.”
He shook his head slowly, pondering.
“I often doubt, I often doubt, the worthwhileness of reason. Dreams must be more substantial and satisfying. Emotional delight is more filling and lasting than intellectual delight; and, besides, you pay for your moments of intellectual delight by having the blues. Emotional delight is followed by no more than jaded senses which speedily recuperate. I envy you, I envy you.”
He stopped abruptly, and then on his lips formed one of his strange quizzical smiles, as he added:
“It’s from my brain I envy you, take notice, and not from my heart. My reason dictates it. The envy is an intellectual product. I am like a sober man looking upon drunken men, and, greatly weary, wishing he, too, were drunk.”
“Or like a wise man looking upon fools and wishing he, too, were a fool,” I laughed.
“Quite so,” he said. “You are a blessed, bankrupt pair of fools. You have no facts in your pocketbook.”
“Yet we spend as freely as you,” was Maud Brewster’s contribution.
“More freely, because it costs you nothing.”
“And because we draw upon eternity,” she retorted.
“Whether you do or think you do, it’s the same thing. You spend what you haven’t got, and in return you get greater value from spending what you haven’t got than I get from spending what I have got, and what I have sweated to get.”
-- Wolf Larsen from The Sea-Wolf by Jack London.
===== The Solution: Egoless engagement with every moment =====
One should become aware of one’s deluded notion in which one thinks that "I belong to these objects of the world and my life depends upon them. I cannot live without them and they cannot exist without me, either" [here objects can be anything that the mind latches onto i.e. animate/inanimate/thoughts/memories/etc.]. Then by profound enquiry, one contemplates "I do not belong to these objects, nor do these objects belong to me" [i.e. the difference between the experiencer, the object experienced and the experience itself]. Thus abandoning the ego-sense through intense contemplation, one should playfully engage oneself in the [everyday] actions that happen naturally [whether due to environment or self-initiated], but with the heart and mind ever cool and tranquil. Such an abandonment of the ego-sense and the conditioning is known as the contemplative egolessness.
Live in the present, with your consciousness externalized momentarily [i.e. egolessly immersed in the current activity for however short/long a time period] but without any effort [i.e. without fixating on the outcome]; when the mind stops linking itself to the past and to the future, it becomes no-mind. If from moment to moment your mind dwells [only] on what is [currently being done] and drops it effortlessly at once [when it is done but before moving on to something else], the mind becomes no-mind, full of purity.
They who, though remaining established in equilibrium, do not let their organs function naturally as long as the body is alive, are obstinate and stubborn people. As long as there is sesame there is oil; as long as there is the body, there are the different moods also. He who rebels against the states that the body is naturally subject to, cuts space to pieces with a sword [i.e. a futile and foolish endeavour]. The equilibrium of yoga is for the mind, not for the organs of action and their states. As long as the body lasts, one should let the organs of action perform their proper function [naturally; without desire/intent/volition], though the intellect and the senses remain in a state of equanimity. Such is the law of nature, to which even the gods are subject.
-- The Yoga Vasistha translated by Swami Venkatesananda.
=====
What are neutrinos good for? - https://www.youtube.com/watch?v=-6iyyM5XRx4
Ice at kilometer level depths is exceptionally clear and transparent since the pressure (from layers above) removes any air bubbles and hence any Cherenkov radiation due to neutrino interaction does not get scattered. This means observations can be done clearly and precisely.
Finally, the rigidity of Ice can hold the sensors precisely and the depth guarantees that no unnecessary external noise from the surface can affect the measurements.
All the above are ideally met by the Ice at the south pole and hence the IceCube Neutrino Observatory was established there.
So in my mind i map your comment as; the "carrier signal" single analog frequency is the infinitely repeating regular wave (no information) traveling at v(p) while the "information signal" (analog/digital) imposed on top of it (frequency/amplitude/phase modulation) creates the informational pulse/wave packet traveling at v(g).
Add in different media in the real world and you have a difference between v(g) and v(p) - https://news.ycombinator.com/item?id=49988070
1) Non-Dispersive medium (eg. vacuum) : v(g) = v(p) = c
2) Normal Dispersion medium (eg. in water) : v(g) < v(p)
3) Anomalous Dispersion medium (eg. absorbing materials) : v(g) > v(p)
where (simplified);
v(g) : group velocity which can be thought of as a function of the overall wave packet (i.e. pulse) and hence contains the actual energy/information/signal.
v(p): phase velocity which can be thought of as a function of a single wave frequency and hence the crest of that wave.
Here is the relevant chapter from the Feynman lectures, Relativistic Effects in Radiation - https://www.feynmanlectures.caltech.edu/I_34.html
If you ask AI, you will get a list with nice short explanatory notes; check it out.
Finally on a related and very interesting vein, Physicists have even brought light to a standstill in tiny gas clouds of sodium atoms cooled to near absolute zero! See the pdf of Scientific American article "Frozen Light" by Lene Vestergaard Hau from her publications webpage - https://groups.seas.harvard.edu/haulab/publications/HauPubli...
This question in the field of "general problem-solving" (inventions etc.) was investigated by studying patent literature by Genrich Altshuller in the former Soviet Union and systematized as TRIZ - https://en.wikipedia.org/wiki/TRIZ
Theory of inventive problem solving' is a methodology which combines an organized, systematic method of problem-solving with analysis and forecasting techniques derived from the study of patterns of invention in global patent literature.
TRIZ developed from a foundation of research into hundreds of thousands of inventions in many fields to produce an approach which defines patterns in inventive solutions and the characteristics of the problems which these inventions have overcome.
See also my older comment for more resources - https://news.ycombinator.com/item?id=45976697
It is the "phase velocity of light in that medium" that is exceeded.
phase velocity of light in a medium = speed of light / refractive index of the medium.
Thus the EM wave is slowed down in a medium and so a charged particle can exceed it producing Cherenkov radiation. This is similar to a sonic boom in atmosphere when speed of sound is exceeded. In both cases the object is traveling faster than the wavefront.
It is only in vacuum that "phase velocity of light" = "group velocity of light" = c (i.e. 300,000 km/sec)
What really is the speed of light in a medium/vacuum, group or phase velocity? - https://physics.stackexchange.com/questions/450377/what-real...
Have you looked at adding Formal Specification/Verification to the above checklist?
It is really nice that you studied both Martin Uecker and Daniel Hooper's techniques and tweaked them to suit your ideas/taste.
I really don't understand why people bring up other languages when one is discussing implementation of some "advanced/tricky/hackish/new" features in C. It is not as if the implementer does not know about the ease of availability in other languages but there is always some set of criteria which prevents switching to a new language.
On a related note, there is a dearth of written/learning material (books etc.) cataloging and explaining advanced architecture/design/implementation patterns in C though we know they exist in the tons of industrial-strength codebases out there.
There is also the fact that when you see an implementation in C of some feature from another language you better understand language design pragmatics eg. implementing inheritance and virtual functions in C gives you insight into how they work in C++/Java/C#/etc.
I also posted your "Adding Reflection to C" at https://news.ycombinator.com/item?id=49964525 and hope HN picks up on it and has a decent discussion.
You definitely should add a detailed post on your "DrC" compiler/interpreter; usecase, scope, techniques used etc. Since this is looking forward to C2y/C29 with some more extensions, i think people will enjoy playing with it in the REPL format.
He also has other interesting C techniques, namely;
Adding reflection to C - https://news.ycombinator.com/item?id=49964525
_Generic for Type Reification in C - https://www.davidpriver.com/creification.html
See also his C2y interpreter with REPL named "DrC" for the upcoming C29 standard (https://en.wikipedia.org/wiki/C29_(C_standard_revision)) - https://github.com/drpriver/drc
PS: I really like his style of writing and presentation; concise and precise without unnecessary fluff and page beautifying.
Visual Thinking in Mathematics: An epistemological study by Marcus Giaquinto - https://academic.oup.com/book/11260
From the Preface:
This book is not a mathematical text` a la Hilbert and Cohn-Vossen, not a psychological investigation` a la Hadamard, nor a How-To manual` a la Polya. It is a work of epistemology. But unlike almost all other writing in epistemology of mathematics, it is constrained by results of research in cognitive science and mathematics education. So the book has interdisciplinary roots.
“I will be honest: We keep finding things that are mysterious, even unsettling,” he said. “We find structures that mirror results from human neuroscience. We find evidence of introspection. We find internal states that functionally mirror joy, satisfaction, fear, grief and unease. I don’t know what that means, but I think it warrants ongoing discernment.”
Chris Olah works on "Mechanistic Interpretability" (https://en.wikipedia.org/wiki/Mechanistic_interpretability) and therefore makes absurd claims based on mere parallels (if any).
See also A Comprehensive Mechanistic Interpretability Explainer & Glossary for some detailed background - https://dynalist.io/d/n2ZWtnoYHrU1s4vnFSAQ519J
"Consciousness" in Humans is a form of "I Know It when I See It" threshold condition (https://en.wikipedia.org/wiki/I_know_it_when_I_see_it) since it is based on self-experience and then extrapolated to other members of our own species.
Whether that same attribute can be applied to other living species (from our pov) which share our planet is not accepted universally. Aspects of it certainly, but the whole as we experience it is denied to them.
The same is applicable even more absolutely when it comes to AI machines.
As regards Morality/Ethics/etc. uniquely "Human" attributes, they are a function of one's effect on the world and hence in so far as machines are allowed to affect the world autonomously, they must be taught to obey our Morals/Ethics as Rules to be followed i.e. a form of "operant conditioning"(https://en.wikipedia.org/wiki/Operant_conditioning) and "methodological behaviourism"(https://en.wikipedia.org/wiki/Behaviorism#Varieties) applied to AI training.
No anthropomorphizing and hand-wringing needed.
1) Math Made Visual: Creating Images for Understanding Mathematics by Claudi Alsina and Roger Nelsen - https://bookstore.ams.org/CLRM/28
2) Roger Nelsen has also written other similar works like the Proofs without Words(3-vols), Nuggets of Number Theory: A Visual Approach, Cameos For Calculus: Visualization In The First-year Course, etc. - https://bookstore.ams.org/browse?Author=%22Roger%20B.%20Nels...
Compilers for all languages have the concept of "lowering" the level of source-language abstractions from high-level to low-level viz. Written Source -> Simpler Source -> AST -> IR -> Machine Code. One type is "desugaring" i.e. transforming complex syntax to simpler ones so that the following stages of compilation have to operate only on a smaller and hence more manageable language subset.
This tool shows both desugaring and other lowering (eg. implicit transformations, type deductions etc.) within the C++ source language by regenerating the source from the AST thus giving you full visibility until that stage in the compilation process.
PS: Explanatory video presentation by the author - https://www.youtube.com/watch?v=VJ6ZvDRYzNE&t=558s
Validating a Lean Proof - https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Excerpt:
The Rosetta Stone
Before diving into syntax, it helps to establish the translation between mathematical and programming concepts. Every idea in formal mathematics has a direct programming analogue.
A theorem is a function with a type signature. Its hypotheses are function parameters, and its conclusion is the return type. The proof is the function body — the implementation. A lemma is a helper function. ∀ (for all) is a generic type parameter. The arrow → means both "implies" and "function from A to B." Conjunction ∧ is a tuple. Disjunction ∨ is a tagged union. Existence ∃ is a dependent pair. Equality = is structural equality. And QED — the moment the kernel accepts the proof — is the moment the type checker says "this compiles."
Thine Church sits alongside "The Church of Edsger Dijkstra" and his Predicate Calculus and Program Semantics is its bible.
Syntax is but mere "ashes and dust" while Semantics are "eternal"!
And brother; hast thou forgotten "The Church of Logic Programming"?
Ruled over by its venerated Pope, Robert Kowalski, who verily laid out its commandments in Predicate Logic as Programming Language and gaveth also the text espousing its central dictum, Algorithm = Logic + Control.
Thine faith must needs be strengthened ;-)
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
But i could not find Thibaut Lutz's presentation slides linked to in the above discussion. Any idea where i can find it?
I presume the control flow in the above presentation is the same as found in "The CUDA Compilation Trajectory" chapter in the NVCC documentation (cudafe++ is EDG) - https://docs.nvidia.com/cuda/cuda-compiler-driver-nvcc/index...