Not using that same subset, however (unless working with a Self-Verifying Theory [0]).
316 karma · joined September 24, 2013
Which is to say, what is the relation between a sub-Peano logical system that can prove itself consistent, and is complete, thus bypassing the 2nd Incompleteness Theorems, and self-referential decision problems posed in the programming language that corresponds to that logical system?
My suspicion is that such a language could provide very strong guarantees on the auditability of self-modifying code.
[0] https://en.m.wikipedia.org/wiki/Self-verifying_theories
[1] https://www.semanticscholar.org/paper/Breaking-through-the-n...
"1. We want to sing of the danger of love, the daily creation of a sweet energy that is never dispersed.
2. The essential elements of our poetry will be irony, tenderness and rebellion."
vs.
"1. We intend to sing the love of danger, the habit of energy and fearlessness.
2. Courage, audacity, and revolt will be essential elements of our poetry."
By any measure of thumos [0], they are incomparable.
Regarding [1], "circularity" in an uncountably infinite context seems different than "self-referential", though the latter is usually geometrically analogized as the former. I tentatively consider Yablo's Paradox to demonstrate that an ineradicable cycle of alternating truth-assignments is equivalent to an infinite (>= aleph-one) regression of alternating truth-assignments, and thus that circularity does not map coherently to self-reference in all logic systems.
[0] http://www.mit.edu/~yablo/pwsr.pdf
[1] http://ferenc.andrasek.hu/papersybprx/jcbeal_is_yablo_non_ci...
Inter-operation between decoupled "small abstractions" and their composed descendants requires either a pre-existing mutual interchange form, or a set of wrappers that provide the same. This is equivalent to simply building on top of that common normal form, which exists, at varying levels of specificity and accessibility, whether one explicitly considers it or not [1]. This, combined with the ultimate CNF still being natural language, because computational semantics are still ultimately evaluated in the context of the human brain, argues for intentionally clarifying and improving that least common computational denominator, in the same way that if one entirely lapses in their recollection of higher synthetic geometry, "begin by assuming a compass and straightedge" is at the least never incorrect.
[0] https://news.ycombinator.com/item?id=13669033
[1] E.g. the cons example in the article is a small abstraction that composes well, at the abstract level, with the cond abstraction for destructuring quoted symbol lists when writing interpreters, but as noted by the author leaks too much of the underlying machine primitives, and thus is an impedance mismatch when seeking performance optimizations, as in a compiler.
http://www.aleph.se/andart/archives/2014/02/torusearth.html
Perhaps this Anders would be interested to discuss the particular brand of paint you enjoy watching dry [0].
[0] Which if one has any fascination at all with viscous fluids or amorphous solids, one really must try sometime.
[0] urbit.org
For my own curiosity, to which languages do you allude in this statement?
[0] Not immediately, but ultimately.
Also, if your Hacker News activity is any representative proxy, you seem like a pretty cool person [0] in general [1]; I would hope to talk with you some thread, should a suitable post of common interest be submitted.
[0] That is, possessing similar affinities to me.
[1] I hope you will not begrudge such a public declaration, but I do not know of any of your more direct means of contact.
For the more knowledgeable, is (symbol-access) a complete general purpose primitive for reactive programming, like (delay) and (force) are for laziness?