HNHacker News
TopNewBestAskShowJobs

jkhdigital

3,636 karma · joined August 31, 2019

submissionscomments
jkhdigital··on LLMs are making formal software verification feasible at a much larger scale
Never change HN, never change
jkhdigital··on The alien space of science: Coherent but cognitively unavailable directions
I was really impressed by the scale of the lacuna tool you created, but then I dug into the niche topics (steganography, covert communication) that constitute my PhD research area and my expectations were tempered.

There’s a lot of noise in the research literature. Lots of papers get published that really don’t contribute much of anything to the field, but the existence of a bunch of papers often sends a signal that some concept is important and needs to be studied.

I find that often a big cluster of papers around a particular topic, none of which seems to move the needle much, is actually an indication that we need a new approach and writing more and more incremental papers just digs deeper into a local minimum.

jkhdigital··on Auto Research: Integer multiplication below n log n
No, lookup tables aren’t magic. The lookup table is part of the program and the execution time includes reading the program itself. A table of size 2^n takes O(2^n) to read into memory.
jkhdigital··on The Slow Formation of Durable Software
How about fast software that works for 10 years?

The difference between an academic and an engineer is that the engineer understands that time spent in research and design does not magically justify itself. Quality and time-to-market are both important and to be an engineer is to figure out how to deliver along the optimal frontier.

jkhdigital··on The Slow Formation of Durable Software
But if you want a cathedral…?
jkhdigital··on The Slow Formation of Durable Software
Keep up the good work. Your contrarian comments on this thread are saving me from wasting time being the contrarian myself.

Is Zotero good software? Yeah, it seems pretty good. I myself don’t use it, despite trying, because it didn’t solve my problems. It is free, has always been free, and its users are primarily academics who do not face market economics for their work output.

Speed is not the enemy. A good engineer knows that time is a precious resource, just like any other, and should be valued appropriately. And engineers are not academics.

jkhdigital··on The Slow Formation of Durable Software
This post smells a lot like academia. I say that as someone who has spent quite a bit of time there myself, so I understand where the author is coming from, but “ivory tower” is still an apt metaphor.
jkhdigital··on Agents don't need memory, they need documentation
Treat it like any other software system: rules that must not be violated are enforced by static type-checking or a trusted runtime monitor. There’s no other option.
jkhdigital··on Context Language Models
Bitter Lesson showing up yet again, this time in context management?
jkhdigital··on A beginning for mathematics
Yes, I have a few CS papers on arxiv myself.
jkhdigital··on A beginning for mathematics
> resulting in the production of an abundance of PDFs. The contents of some of those PDFs may even have important applications.

I hope, from the depths of my soul, that the static typeset report format for transmitting knowledge and understanding will finally die and be laid to rest.

jkhdigital··on Stabilizing Rust's Never Type
Java doesn’t permit that. You must specify covariant or contravariant type parameters with <? extends T> or <? super T>.
jkhdigital··on A few good ideas in programming languages
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.
jkhdigital··on A few good ideas in programming languages
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 point I think we have good solutions for expressing pretty much all the most common program semantics, but there’s no language that brings them all together under a unified syntax, tooling, etc.

jkhdigital··on A few good ideas in programming languages
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.
jkhdigital··on The browser's main thread is expensive
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, but I think it is a bit behind the ball in framing scheduling problems as a matter of “experience and judgment”. The problem of allocating work to a scarce resource is one of the oldest and most well-studied in all of computer science. It would make sense to go consult a textbook on the matter before trying to reinvent the wheel.

jkhdigital··on Show HN: The load-bearing vocabulary of Claude
“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.
jkhdigital··on AI boosted homework scores, then exam scores dropped: study
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 a given student is comprehensive assessment. Bad assessment design, much like bad experiment design in science, is worse than useless—it actively misleads and confuses.

A well-designed, repeatable, reliable assessment is a prerequisite before one can even consider the effects of particular pedagogical methods inside or outside of the classroom itself.

jkhdigital··on Everyone says assembly is untyped—everyone is wrong
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 explicitly declared by the caller. The type declaration is all about possible side effects.

It’s an effect in the type system, not a data type or behavior.

jkhdigital··on Everyone says assembly is untyped—everyone is wrong
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 level.

I suspect the main reason someone might quibble over the “assembly is typed” assertion is that many programmers have a rather narrow view of type systems, heavily skewed by OOP patterns.

jkhdigital··on AI boosted homework scores, then exam scores dropped: study
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 always suffered from a unit economics problem: the labor required to assign individually-tailored problem sets and manually grade them in the volume needed for most students to actually learn the material is prohibitively expensive.

jkhdigital··on AI boosted homework scores, then exam scores dropped: study
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 concluded that academia is actively resistant to implementing assessment reform because it would expose the utter pointlessness of most of what happens in university classrooms.

The reality is that we have no idea what most university exams measure because they are ad hoc, written by amateurs (yes, most professors are untrained in pedagogical methods) with zero psychometric validity analysis.

jkhdigital··on Programmable Property-Based Testing
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 generator (in the style of https://dl.acm.org/doi/10.1145/3158133) so that this optimization is at least available only when proven sound?
jkhdigital··on The Case Against Formal Verification, 50 Years Later
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 portability and modularity and extensibility.
jkhdigital··on LLMs reward expertise
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.
jkhdigital··on LearnVector – Andrew Ng's AI company building one‑to‑one learning experiences
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 follow MA’s example as I put together curricula for my undergraduate CS courses.
jkhdigital··on LearnVector – Andrew Ng's AI company building one‑to‑one learning experiences
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 objectively assessing skill mastery. Most learners don’t want to learn for its own sake, they want a credential that proves their value to potential employers. All of the value in learning accrues to the credential, and everyone in the educational establishment is quite happy reserving that privilege for the accredited universities because they can just bundle more and more products and services into the tuition sticker price without ever having to justify it. Oh, and the student loan racket ensures that enough students are price-insensitive that they’ll never look for alternatives.
jkhdigital··on LearnVector – Andrew Ng's AI company building one‑to‑one learning experiences
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. Stanford, Harvard and MIT can do whatever they hell they want in the classroom as long as they continue to skim the cream of each generation and no objective assessment exists to demonstrate that they contributed nothing above what their exceptional students probably would’ve done in four years anyway.
jkhdigital··on LearnVector – Andrew Ng's AI company building one‑to‑one learning experiences
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 development. For essentially all knowledge-based skills, what’s missing is the core foundational skill progression that leads to actual mastery.

How many different personal training styles do you see for competitive sports? There’s variation, but only at the margins. Nobody deviates from the essential training core because doing so leads to poor performance and competitive failure. And yet we have a total free-for-all in knowledge disciplines where we just throw untrained PhDs in front of a classroom and assume they’ll produce results. Oh, and we also provide zero tangible incentives for them to improve learning outcomes.

jkhdigital··on LearnVector – Andrew Ng's AI company building one‑to‑one learning experiences
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 environment that more or less requires them to commit to studying until mastery or to quit early and do something else.

Effective learning techniques have been known for decades, but universities have -zero- incentive to improve teaching quality. There is no standardized assessment infrastructure to compare graduates across schools, or to evaluate the effectiveness of teaching interventions at scale. So any effort put into teaching quality is invisible and thus worthless to a university.

Every attempt to make high-quality instruction available for free has been largely irrelevant to the unwashed masses, because universities have a monopoly on credentialing. The self-starters can learn anything for free, but they were never the problem. It’s the middle 50% that we have utterly failed.

Page 1 of 34Next →