There is a weird disconnect between the first part of the post, which suggests that we should de-emphasize applications and can now focus on “the beautiful ideas, the insights, the beauty”, and then the second half, which presents the following three examples:
Getting a machine to generate a possibly-correct (who knows?) declarative description of a programming language from an implementation of the language.
Helping Amazon verify their proprietary software faster by adding LLMs in their verification tools.
Asking a machine to produce a declarative specification of a programming language in a problem domain that we don’t understand, because we do not allow ourselves to spend the time to learn it (but can still serve as an expert to help the system authors assess the resulting spec).
I am sure that being able to work on all of these faster than before can be exciting and satisfying – this is the main point of the article. But I fail to understand how they relate to the proposal of worrying less about applications/adoption and focusing more on things that are beautiful and insightful.
(I also think that the post is tone-deaf and weird as a follow-up on the TYPES discussion, but oh well, this is a discussion to have with the author.)
There is a weird disconnect between the first part of the post, which suggests that we should de-emphasize applications and can now focus on “the beautiful ideas, the insights, the beauty”, and then the second half, which presents the following three examples:
I am sure that being able to work on all of these faster than before can be exciting and satisfying – this is the main point of the article. But I fail to understand how they relate to the proposal of worrying less about applications/adoption and focusing more on things that are beautiful and insightful.
(I also think that the post is tone-deaf and weird as a follow-up on the TYPES discussion, but oh well, this is a discussion to have with the author.)
score 5 · canonical