jkhdigital

7 ms·

1.
by jkhdigital 4d ago
Java doesn’t permit that. You must specify covariant or contravariant type parameters with <? extends T> or <? super T>.
2.
by jkhdigital 4d ago
We don’t need new ideas, we need languages that take the best ideas developed over the past decade of PL research and operationalize them in a language with modern tooling and build support.
3.
by jkhdigital 4d ago
Most of my research conversations with Claude nowadays are basically about this—what it would take to make every latent bit of program semantics visible and expressible in the language itself. As you put it, first-class everything. At this
4.
by jkhdigital 4d ago
I think Pony’s reference capabilities are a better solution for linear types. It’s just part of the language so a violation is simply a type error, not something flagged later during static analysis.
5.
by jkhdigital 13d ago
This article concludes with the following statement: > So much of development is trade-offs, and you have to choose according to the situation, which ultimately comes down to the developer’s experience and judgment. It’s a great article,
6.
by jkhdigital 19d ago
“non-trivial” is one of those words that seems like it should be a Claude-ism but is actually just the single best word for a concept that comes up extremely often in research and engineering discussions.
7.
by jkhdigital 25d ago
You’re conflating the course and the classroom. The explicitly stated goal of most courses is mastery of a well-defined set of domain-specific knowledge and skills. The only way to objectively determine if the course achieved that goal for
8.
by jkhdigital 25d ago
Assembly doesn’t have typed objects, it has typed instructions. It’s like checked exceptions in Java—you have to declare them in the type signature of the method, and the compiler enforces that they are either caught and handled, or also ex
9.
by jkhdigital 25d ago
In other words, the type of an assembly instruction specifies its effects and coeffects. This is an active research area—describing effects and coeffects in the type system, and discharging handler/provider obligations at the compiler
10.
by jkhdigital 26d ago
The problem was never the volume of homework, it is the targeting and specificity. Learning happens through repetitive deliberate practice, full stop. You can’t learn through osmosis; effort is required. Industrialized mass education has al
11.
by jkhdigital 26d ago
I just started teaching undergrad CS courses after ~20 years of various non-academic jobs and it took me about two semesters to realize that almost nothing matters except how I assess students. Two weeks of ADHD-fueled research later, I con
12.
by jkhdigital 29d ago
In section 6.1 you mention experimenting with bypassing the precondition checks for correct-by-construction generators. Have you considered giving this "unsafe" runner a type that demands a completeness certificate for the gener
13.
by jkhdigital 1mo ago
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are porta
14.
by jkhdigital 1mo ago
But the guy who writes the “just do it” prompt can neither formulate the conjecture in the first place, nor come up with any follow-up questions to build on the result.
15.
by jkhdigital 2mo ago
Math Academy is doing it right. Their neat synthesis of spaced repetition and the knowledge DAG is slick, but honestly the extremely fine-grained skill decomposition is what’s missing in virtually all of higher education. I’m trying to foll
16.
by jkhdigital 2mo ago
The dirty little secret of EdTech is that there is no money in improving learning because there is no way to capture the value. For all but a handful of highly specialized and insular professions, there is no scalable infrastructure for obj
17.
by jkhdigital 2mo ago
Most people don’t want to learn, they want a credential. The real hard problem here, that has been sidestepped for decades and decades, is how to gate credentials behind standardized skill assessments rather than branded gatekeepers. Stanfo
18.
by jkhdigital 2mo ago
Yep. Literally every EdTech idea is a rehashing of the same flawed reasoning: we just need better monitoring and metrics to manage everyone’s learning process! No. Learning comes from repetitive deliberate practice in the zone of proximal d
19.
by jkhdigital 2mo ago
This is exactly right. I started teaching undergrad CS about 18 months ago after 20 years wandering through other careers, and I quickly realized that students do not need better teaching. They need frequent, direct feedback and an environm
20.
by jkhdigital 2mo ago
This is my exact experience right now trying to wade through the research on psychometrics and skill/knowledge assessment design. It’s mostly just applied statistics but like all such fields, over decades of specialization it acquired
21.
by jkhdigital 3mo ago
Saw this comment at the top with 0 replies and thought “How is that possible??” and then saw the “0 minutes ago” timestamp. Only on HN can you stumble into the comments section just moments after a CTO, founder, author, etc. left unfiltered
22.
by jkhdigital 3mo ago
I love this kind of thing—going to try and use this in my data structures course.
23.
by jkhdigital 3mo ago
Not sure about the significance of the result here, but this article just gave me the inspiration I needed to solve Project Euler #202: https://projecteuler.net/problem=202
24.
by jkhdigital 4mo ago
At this point I think the category theorists hit the foundational idea squarely on the mark: 1. Start with a few simple but non-trivial terms and axioms 2. Define "universal constructions" as procedures for building uniquely ident
25.
by jkhdigital 4mo ago
I'm going to first apologize for engaging in rhetorical sleight of hand myself, since I indulged in a bit of the hand-wavy argumentation that happens so often in these nit-picky debates. I'm going to respond cleanly here mostly to
26.
by jkhdigital 4mo ago
Right, the crazy thing is that much of the groundwork for the “rules-and-heuristics” mode of AI was laid down in the 70s and 80s, long before we had the raw compute power to reliably extract patterns from reality-scale inputs. Those early e
27.
by jkhdigital 4mo ago
No, you’re using the same sleight of hand as the paper. Boebert’s objection is about whether Alice can transmit unauthorized authority to Bob across a security boundary that’s supposed to prevent that flow. Your SCM_RIGHTS example is a case
28.
by jkhdigital 4mo ago
Covert channels are a thing. Shared access to resources always opens the possibility of covert information passing through e.g. modulation of resource usage. This isn’t even out-of-band, it’s just a hard fact that a shared resource always
29.
by jkhdigital 4mo ago
I’m not going to argue against much of the content of this paper, but it should be pointed out that their argument in the middle section against the “confinement myth” seems pretty bogus. They say that you can isolate the capability read&#x
30.
by jkhdigital 5mo ago
Let me know when you have enough demand to make it multiple full-time jobs. I’ve been making notes for a few years now about all the best patterns and principles for designing complex systems and your language + engine more or less hits all

More ›