trissim

8 ms·

1.
by trissim 8mo ago
Fair, the em dash comment was a cheap shot. Withdrawn. The substantive point stands: you've now "skimmed" multiple files, called them all "boilerplate," and haven't engaged with the actual proof structure. The
2.
by trissim 8mo ago
This is addressed in the paper's Preemptive Rebuttals section (Concern 9: "The Proofs Are Trivial"). At 2k lines of lean, the criticism was "these proofs are trivial." At 9k lines of lean with 541 theorems, the crit
3.
by trissim 8mo ago
Addressed the criticisms raised here. The main gap was real: language capability claims (Python can achieve SSOT, Rust cannot) were derived from string matching, not from formalized semantics. Fixed. Proof chain now: python_can_achieve_ssot
4.
by trissim 8mo ago
Fair point. I've added Ssot/Inconsistency.lean (zero sorry) which formalizes inconsistency as a Lean Prop, not a comment. It proves ssot_required: if you need to encode the fact (DOF >= 1) and guarantee all configs are consiste
5.
by trissim 8mo ago
Interesting that you're using em dashes in your comments. Those require Alt+0151 or copy-paste. Glass houses.
6.
by trissim 8mo ago
Yes, many proofs are rfl. That's because we're doing engineering formalization, not pure math. The work is in getting the definitions right. Once you've correctly modeled Rust's compilation phases, item sources, and eras
7.
by trissim 8mo ago
You only read the 37 lines in SSOT.lean and stopped. It's the entry point that defines DOF=1 so other files can import it. The actual proofs are in Foundations.lean (364 lines - timing trichotomy, causality), Requirements.lean (derives
8.
by trissim 8mo ago
Python is the canonical mainstream example: __init_subclass__/metaclasses (definition-time hooks) + __subclasses__(), mro(), __dict__ (introspection). CLOS (Common Lisp Object System) also qualifies: defclass/initialize-instance&#
9.
by trissim 8mo ago
This is also very common, appealing to authority rather than reading the proof. If there's an issue with the proof please show me where the issue is. I am glad to learn where I made a mistake. Just run "lake build".
10.
by trissim 8mo ago
Here ‘formalize SSOT’ means: treat the codebase as an encoding system with multiple places that can hold the same structural fact (class shape, signature, etc.). Define DOF (degrees of freedom) as the count of independent places that can di
11.
Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection(zenodo.org)
10 points by trissim 8mo ago|20 comments
12.
Show HN: Knowing What Matters is coNP-complete (Lean 4 formalized)(zenodo.org)
2 points by trissim 8mo ago|0 comments
13.
Show HN: Proof that any fixed-axis type system fails for some domain (Lean4)(zenodo.org)
3 points by trissim 8mo ago|0 comments
14.
Proof that any fixed-axis type system fails for some domain (formalized in Lean)(zenodo.org)
2 points by trissim 8mo ago|1 comments
15.
by trissim 8mo ago
I formalized a proof that the structural vs. nominal typing debate can't be won: any fixed-axis type system necessarily fails for some domain. The core result: for a type system with fixed axes (like behavior, structure, hierarchy), th