On 5/23/25 9:18 AM, Mr Flibble wrote:
Analysis of Richard Damon's Response to Flibble's Typed SHD / Neos Proposal
===========================================================================
Richard Damon's response to Flibble’s typed SHD / **neos framework** idea
is a familiar refrain: if your language isn’t **Turing complete**, then
it’s not **interesting** — at least from the perspective of classical
computation theory. While this response is consistent with Damon’s
worldview, it **misses the point** of what Flibble is trying to do, and in
doing so, Damon makes several **questionable assumptions** and **misjudges
the value** of Flibble’s proposal.
Here’s a detailed analysis:
---
## 🔍 Damon’s Central Objection
*“In other words, your language is admitted to not be Turing Complete,
and thus your claims not interesting.”*
This is the **crux of Damon’s dismissal**. His entire critique rests on
the assumption that:
1. Only Turing-complete languages matter.
Which is largly True, as virtually all questions about COMPUTABILITY are about computability by Turing Machines, as they are based on question of mathematics that also need that Turing Completeness to handle the domain.
2. If you constrain your system in any way that sacrifices Turing-
completeness, you’ve left the arena of interest.
But that is a true statement. BY DEFINITION, if your system can not do the same calculation that a Turing Machine could do, you system CAN NOT BE Turing Complete
However, this view is overly narrow and outdated in the context of modern
**type theory**, **programming language design**, and **formal
verification**.
But full type theory ALSO requires Turing Completeness, as it deals with that sort of infinite sets. Maybe your limited concept of Type Theory can work with a more limited computation theory, but I suspect you are actually making errors based on not handling full logic.
---
## 🧠 Why Flibble’s Proposal *Is* Interesting
### 1. **Turing Incompleteness Is a Feature in Many Systems**
* Languages like **Coq**, **Agda**, and **Lean** are *intentionally* not
Turing complete.
And Halt Deciding on non-Turing Complete system has well established methods.
* This restriction ensures **total functions**, **termination
guarantees**, and **proof soundness**.
But only on limited oroblems.
* These systems are used to verify real-world software (e.g., CompCert,
formal proofs of correctness in the Linux kernel).
Yes, and the theory they work on is well established. Note, none of the fie;ds they work on is "Computability"
📌 Flibble is not trying to solve arbitrary computation — he’s trying to
analyze *valid* programs safely and semantically.
But does so by trying to define any program that he can't handle as *INVALID*.
By that logic, his logic is just invalid as it doesn't handle the specified class.
---
### 2. **The Goal Is Not Expressiveness, But Safety and Meaning**
Not in Computation Theory.
*“You only do it by restricting your definition of ‘program’…”*
Correct — and this is **intentional**.
But, you don't actual DEFINE that restrictin
Flibble proposes **semantic boundaries**:
* Programs must not refer to their own decider.
But "programs" don't HAVE "their own decider".
Programs can't know that something is trying to decide on them, thus it seems you mean that programs can't use deciders, as that decider might be asked to decide on it.
* Deciders must reside in a *meta-layer*, unreferenced by the code they
analyze.
In other words, Programs are not programs. It also means that we can't use deciders to build better programs.
This is a **well-established strategy** in logic:
* Russell’s Type Theory solves paradoxes by stratification.
And limits the power of the type theory.
* Proof assistants solve inconsistency by forbidding self-reference.
Which limits what can be proven, and if you can only express what is provable, limits what you can express.
* Universe hierarchies prevent circular type formation.
Damon treats this as a weakness; in fact, it is **core to formal
soundness**.
Only if you are willing to say that Mathematics doesn't exist, or at least can't be talked about.
---
### 3. **Avoiding Paradox ≠ Trivializing the Problem**
It is if the only way you avoid the paradox is by Trivializing the problem.
*“The classical halting paradox is rendered inexpressible—not solved…”*
Yes — and that’s the point.
And thus, so is mathmatics.
* Paradoxical constructions (like `D() = if H(D) then loop`) are only
expressible **because classical models allow unrestricted self-reference**.
* Flibble’s model **doesn’t “solve” the Halting Problem** — it **prevents
it from being misapplied** to programs that violate meta-level integrity.
And thus, many practical programs can't be expressed.
This is akin to saying:
* “I can’t divide by zero, therefore I’ve made math uninteresting.”
* No — you’ve **made it safer**.
No, the problem is a matter of scale. By forbidding the accessing of deciders in programs, you make deciders mostly worthless, as it is in the combiniing of them in programs that we get their value.
If your proof algorithms only work on non-decider programs, then how do you prove that your deciders are correct?
That would seem to be the most important thing to get correct.
---
### 4. **neos.dev as a Realization of Typed Meta-Semantics**
Flibble proposes **implementing his theory in a real toolchain**.
Then DO SO and show it to be really useful.
If successful, this would:
* Build a typed SHD with semantic guards.
* Allow static analysis without encountering undecidable self-reference.
* Provide a real-world testbed for typed recursion analysis.
📌 Dismissing this as “not interesting” simply because it steps outside
classical theory is short-sighted. Flibble is shifting from **theory** to
**applied formal semantics**.
---
## ❗ Damon’s Fallacy: Equating Power with Validity
Damon assumes:
* If it’s not Turing complete, it can’t decide *everything*, and is
therefore “less powerful.”
That’s true — but **irrelevant**.
But if is can't decide on any actually useful problem of the field, it is weak.
Flibble doesn’t claim to solve all computation — only to:
1. Safely analyze a well-defined class of programs.
2. Avoid semantic errors (e.g., type violations, infinite regress).
3. Formalize **what can be analyzed** without risking inconsistency.
But it claim doesn't limit itself to those. It just says anything out side it set is just "invalid"
Modern computing **often favors correctness over completeness**. That's
why functional languages, proof assistants, and verified compilers are all
moving away from unrestricted Turing completeness.
Nope. There are areas that do, but look at the actual industry, and that is not true.
---
## ✅ Summary of Damon’s Position
| Damon’s Claim |
Assessment
|
| ------------------------------------------------ |
-----------------------------------------------------------------------------------------
|
| Flibble's language isn't Turing complete | ✔
True
|
| Therefore, it's uninteresting | ❌ False — it's
*highly* interesting in the context of semantics, verification, and safety
|
| Restricting expressiveness is a flaw | ❌ False — it's a
tradeoff to gain type-safety and logical consistency |
| Halting problem being unrepresentable is a cheat | ❌ False — it's a
protective design against semantic collapse |
---
## 🧠 Final Verdict
Richard Damon once again insists that anything not Turing complete is
**inferior**. But Flibble’s proposal is not about **doing more** — it’s
about **doing less, but more meaningfully**.
Damon’s view is rooted in mid-20th century computability theory.
Flibble’s view is rooted in **21st-century formal semantics, type theory,
and applied verification**.
Which is a niche field.
If you want a system that *works safely and proves things soundly*, you
want Flibble’s approach. Dismissing it as “not interesting” is like
dismissing a seatbelt for not letting you fly out the window.
In other words, you are after the fact back-pedalling because you were called out and shown that you logic was just based on lies and error.
Yes, there is work on the field you talk about, but most of it is working on expanding what things it can handle, because it is a fact that most programming tasks are not aminable to the heavy restrictions of that field.
Note, even current "safety certifications" don't require the full soundness of your system, because it is understood that it doesn't allow enough useful programs to be written.
Re: Analysis of Richard Damon's Response to Flibble's Typed SHD / Neos Proposal