Please help me list math formalization projects looking for volunteers:

https://mathoverflow.net/a/500723/

너무 이른 시점에 일반화를 걱정하는 것은 위험할 수 있습니다. 자신이 코드를 작성하든 다른 사람의 코드를 이해하려 하든, 우리는 이 책에서 취한 접근 방식을 따를 것을 권장합니다. 즉, 일반적인 것부터 시작하지 말고 구체적인 예시부터 시작하세요. 그런 다음 그들이 어떤 측면을 공유하는지 관찰하세요. 학습자로서 이러한 순서는 더 쉬운 구체적인 예시를 토대로 더 어려운 추상적 개념을 이해할 기회를 더 많이 제공합니다. 저자로서 이러한 순서는 더 추상적인 발상이 타당성을 갖고 목적을 지닐 수 있도록 도와줍니다.

— 《Finding Success (and Failure) in Haskell》, 149쪽

https://events.linuxfoundation.org/open-source-summit-korea/program/schedule/?utm_campaign=10983194-Open Source Summit-Korea-2025&utm_medium=email&_hsmi=381732193&utm_content=381732193&utm_source=hs_email

오픈소스 서밋 코리아 세션 리스트 공개됐네요

여러분 int *p를 (int *)(uintptr_t)p 캐스팅하지 마세요 출처라는 것이 바뀝니다

Selection API와 DOM 렌더링 동기화 문제 분석 https://gist.github.com/easylogic/0f4702607982e37077347d44963683f5

LCP, LCS 알고리즘이 이렇게 쓰인다니

이거 아무리 봐도 옛날에 본 심리검사 문항 같다. 이런 느낌으로

@z9mb1wwj @catamorphicCata @msy윤민석 @joonnotnotJoon @d01c2Hyunjoon Kim @icecream_mable구슬아이스크림 @minju2996bbang @2chanhaeng이찬행 @lionhairdino @akastoot악하 @jihyeokJihyeok Seo @linea @woaol벨 @theeluwin제이미 @rangho우주해커 끄적끄적 랭호 📝 @robin @1ho1호 @nebuletoHaze @morealLee Dogeon @harei106Hannah Reinecke @realfishbread최윤희 @jcha0713joohoon @hyunjoon @krepe90남기현 (Krepe) @cetaceanightskyCetacea @aiooAhn Kiwook @ink_punctuation책 읽는 프로그래머 @yg1ee밀

오늘 Hackers' Public 행사 첫번째 모임에 와주셔서 정말 감사합니다! 정말 즐거웠습니다! 잘 들어가세요!

오는 11월 8일 토요일 오전 10시, 광운대학교에서 열리는 FOSS for All 컨퍼런스에 여러분을 초대합니다.

FOSS for All 컨퍼런스는 "Free and Open Source Software for All"이라는 슬로건 아래, 모두를 위한 오픈 소스 컨퍼런스를 목표로 하는 비영리 오픈소스 커뮤니티 주도의 컨퍼런스입니다.

FOSS for All 컨퍼런스는 오픈소스 소프트웨어와 커뮤니티에 관심 있는 누구나 참여할 수 있으며, 개발자, 기여자, 디자이너, 번역가, 기획자 등 다양한 역할의 사람들이 경험과 지식을 공유하는 장으로 기술 발표, 커뮤니티 부스, 패널 토크 등 다양한 프로그램이 마련될 예정입니다.

많은 후원과 참여를 부탁드리겠습니다. 고맙습니다. :-D

#FOSS #오픈소스 #개발자 #컨퍼런스

https://event-us.kr/fossforall/event/110400

Hackers' Pub 티셔츠 주문 받습니다!

오래 전

현대 컴퓨터는 계산기라기보다는 복사 기계에 더 가깝다

는 문장을 읽었고 그것에 대해 종종 생각함. 생각해 보면 정말 하는 일이 대개 그런 것에 속한다고 느낌. 어딘가에 있다는 데이터를 모으고 가공하고 정제해서 또 어딘가에 두고 그걸 누군가 가져갈 수 있게 하는 일 끊임 없이 반복함. 데이터의 형식이나 크기나 여러 속성이 다양하고 그래서 다루는 방법과 기술에도 많은 차이가 있지만 어쨌든. 요즘 종종 인용되는 타입 검사는 해결책이 아니라 증상이다(Type Checking is a Symptom, Not a Solution)에 대한 반응들을 보고 직렬화 글과 거기 인용된 인터넷은 디버깅 모드로 돌아가고 있다는 글까지 떠올랐음.

(이 글은 Hackers' Pub에서 제공하는 Markdown 문법 가이드에 익숙해지기 위한 시도로 작성함.)

〈타입 검사는 해결책이 아니라 증상이다〉(Type Checking is a Symptom, Not a Solution).

난 이 글에 동의하지 않는데, 여러 측면에서 그렇지만, 한 측면에만 집중해서 얘기해 보자면: 좋은 아키텍처는 훌륭한 프로그래머를 요구하지만 타입 시스템은 훌륭한 프로그래머를 요구하지 않기 때문이다.

누구나 훌륭한 프로그래머가 되어야만 하는가? 혹은 될 수 있는가? 좋은 아키텍처를 그릴 수 있는 훌륭한 프로그래머가 아니라면 소프트웨어 개발을 해서는 안 될까? 좋은 아키텍처에만 의존하는 것은 잠재적으로 엘리트주의를 끌어들이기 쉽다: 「어떤 시스템이 오작동하는 것은 아키텍처가 나쁘기 때문이다. 아키텍처가 나쁜 이유는 그걸 설계한 프로그래머가 수준 미달이기 때문이다」와 같이.

반면 타입 시스템은 일단 도입만 하면 누구나 그 덕을 볼 수 있다. 팀 내의 프로그래머들의 역량이 뛰어나든 뛰어나지 않든. 훨씬 평범한 보통 사람에게 유리하다. 타입 시스템이 미봉책일 수는 있지만, 그 미봉책이 더 많은 사람들을 프로젝트에 참여할 수 있게 해준다고 생각한다.

https://contribute-suggestion.vercel.app/
대강 배포는 했어요
프론트 버그가 많아서 고쳐야 하지만 일단 올리긴 올림
깃헙 토큰은 각자 받아서 사용해야 됩니당

지난 몇 달간 htmx로 웹 앱을 만들면서 느낀 점은, 골디락스 존의 하위 50% 애플리케이션에만 htmx가 적합하다는 것이다. 클라이언트 상태를 조금이라도 다뤄야 하는 순간이 오면 불행이 시작된다. 하이퍼미디어 시스템의 철학에 동의하는데, 그 구현은 아일랜드 아키텍처의 접근법이 더 나을 수도 있겠다는 생각이 든다. https://deno.com/blog/intro-to-islands

Here is a first proof-of-concept demonstration of an actual outcome for the erdosproblems/OEIS linkage project. There are a number of Erdos problems relating to irrationality of specific series. I asked an AI to compute several of these series to several decimal places (https://chatgpt.com/share/68b7160a-3d4c-800e-a834-415ee9aac2a8), then entered in these decimal strings into the OEIS search bar. I found several hits, which I then uploaded to the project https://github.com/teorth/erdosproblems/commit/89c3a9c977fd40de74c0ea18d30ff258af053ff3%E2%80%9C .

In particular, I linked Erdos problem 259 https://www.erdosproblems.com/259 to OEIS A371134 https://oeis.org/A371134. In the latter page, there was a reference to a solution to the problem by Chen and Ruzsa https://doi.org/10.1023/A:1004742930674 that was not known to the erdosproblems.com site. So now we can mark that problem as solved!

I think this type of semi-automated literature search could be a good use case for AI tooling, since the (potentially unreliable) output of such AI tools is only used to locate more reliable human-generated resources, rather than being directly incorporated into the final product.

https://keivan.io/the-day-appget-died/

윈도 패키지 매니저 AppGet의 개발자가 WinGet 개발 과정에서 접촉했던 경험을 쓴 글.

MS가 오픈소스 친화적으로 바뀌고 있다고 하지만, 여전히 내부 문화가 매우 관료적이고 사내 정치가 toxic하다고 유명한데, 독립 개발자로서 MS와 컨택하는 일이 어떤 것인지 잘 알려주는 사례라고 봄.

Special thanks 한 줄만 적어줬어도 그가 분노하지는 않았겠지만, 그 한 줄 넣기가 어려운 게 Microsoft겠지.

Tiny Datasette Uses USB For the Modern Day

https://hackaday.com/2025/09/01/tiny-datasette-uses-usb-for-the-modern-day/

혹시 번역본이 편한 분은 여기에 번역본이 있습니다.(notJoon님 말고 다른 분들 보시라고 링크 달아 둡니다.)
https://eatchangmyeong.github.io/2022/12/04/parse-don-t-validate.html
@joonnotnotJoon

I just published a blog post on the use of type-level programming in TypeScript. It was originally a section of the larger post I’ve been alluding to but I broke it out and expanded it. It’s much more of an opinion piece than most things I write but I’d like to think I have a few decent insights in there. Please check it out and let me know what you think.

https://jnkr.tech/blog/expressive-types-tradeoffs

#programming #typescript

look at this big fucking cat ​​

Today is the new semester for @CMUDBCMU Database Group's Intro to Database Systems! We're going harder into material than ever before. Projects are more challenging but you can use LLMs to help. We also have 10min talks each Wed from leading DB companies. Follow from home/prison on YouTube: https://15445.courses.cs.cmu.edu/fall2025

Everything is available for free to non-CMU students:
• Lectures on YouTube: https://www.youtube.com/playlist?list=PLSE8ODhjZXjYMAgsGH-GtY5rJYZ6zjsd5
• Slides + Notes + Homeworks on course website.
• Project source code on GitHub: https://github.com/cmu-db/bustub
• Grading with Gradescope (see FAQ ➡️ https://15445.courses.cs.cmu.edu/fall2025/faq.html#q7)

Special thank you to our Affiliate companies for their support this academic year:
• ClickHouse
• DataStax
• dbt Labs
• Firebolt
• MotherDuck
• RelationalAI
• SingleStore
• SpiralDB
• PingCAP / TiDB
• Yellowbrick
• Yugabyte

Hackers' Pub은 현재 Fresh 프레임워크로 만들어져 있는데, Fresh 프레임워크의 한계를 벗어나기 위해 GraphQL + SolidStart 스택으로 넘어가는 작업(web-next)을 진행중입니다. 진행 상황을 관리하기 위해 에픽 이슈를 만들었습니다.

역시 수제코딩을 해야 감각이 늘고 리터러시가 생긴다..... 뇌에 힘주고 해야하는건 수제코딩..

블로깅의 쇠퇴, AI의 끝없는 학습, 비공개 플랫폼(Discord 등)으로의 이주, 짧고 중독성만을 강조하는 피드와 BM, 한 번 보면 다시 찾기도 힘든 SNS 포스트, 범람하는 가짜뉴스와 개소리와 혐오... 웹은 정보의 망망대해도 아닌 소행성대로 변해가고 있다.

I wrote an op-ed on the world-class STEM research ecosystem in the United States, and how this ecosystem is now under attack on multiple fronts by the current administration: https://newsletter.ofthebrave.org/p/im-an-award-winning-mathematician

네이버플러스 멤버십 해지가 잘 안되어서 고객센터에 전화했다. 몇 차례의 좌절 끝에 비밀통로를 발견했다.

이번에 다익스트라보다 빠른 최단 경로 알고리즘이 나왔다고 해서 논문을 읽어봤는데 역시 어려워서 나가떨어졌다 arxiv.org/abs/2504.17033

Breaking the Sorting Barrier f...

Perl을 만든 언어학자 Larry Wall이 쓴 글 중에 종종 다시 읽어 보는 글

Human languages therefore differ not so much in what you can say but in what you must say. In English, you are forced to differentiate singular from plural. In Japanese, you don’t have to distinguish singular from plural, but you do have to pick a specific level of politeness, taking into account not only your degree of respect for the person you’re talking to, but also your degree of respect for the person or thing you’re talking about.

Programming is Hard, Let's Go Scripting...

그렇기 때문에 사람의 언어는 당신이 그렇다고 생각하고 있던 것과는 많이 다르다. 영어로 얘기할때는 단수와 복수를 확실히 구분해야만 한다. 일본어에서는, 단수와 복수를 구분할 필요는 없지만, 정중함의 정도를 조절할 줄 알아야 한다. 즉, 상대방에 대한 존경을 표현할 수 있는 정도를 선택해야 하고, 상대방의 입장에서 내가 존중 받아야 하는 정도를 생각해서 말해야 한다.

프로그래밍은 어렵다, 스크립팅의 세계로 가보자...

What is the biggest reason that makes you hesitate to adopt #Fedify?

#ActivityPub #fedidev

Hackers' Pub의 로고 디자인이 완료되었습니다! 디자인은 박은지 님(@murinono무리노노)께서 해주셨습니다.

연합우주라는 콘셉트에 맞게 고양이의 입 주변을 별 모양으로, 목 아래에도 고리(orbital ring) 모양으로 디자인했습니다. 고양이를 고른 이유는 소프트웨어 프로그래머 커뮤니티에서 다른 동물보다 유독 고양이가 사랑 받기 때문이기도 하고, 고양이가 호기심이 강하기 때문이기도 합니다.

로고 디자인은 CC-BY-SA 4.0 라이선스로 배포됩니다.

Solid Korea 커뮤니티 디스코드를 오픈해보았습니다! 많은 관심 부탁드려요~~~ https://discord.solid-korea.org

@joonnotnotJoon 반대로 컴파일이 안되면 명세가 아니고 이를통해 가짜 명세를 구분할수있겠지요

🎉 Huge shoutouts to two amazing contributors from Korea's #OSSCA program who just made #Fedify even better!

First, @z9mb1wwj delivered PR #321, adding a handy -o/--output option to fedify lookup. Now you can save lookup results directly to files instead of just printing to terminal—a nice quality-of-life improvement for analysis and scripting workflows.

But the real showstopper is @joonnotnotJoon's incredible PR #283, which introduces the brand new @fedify/testing package! This massive contribution (2,014 lines across 20 files) brings MockFederation and MockContext classes that completely transform how we test federated applications. No more complex setups or actual network requests—just clean, straightforward unit testing with activity tracking, inbox simulation, and queue-aware testing capabilities.

These contributions solve real pain points and showcase the amazing talent emerging from the OSSCA program. Both features will be available in the upcoming Fedify 1.8 release. The future of federated software development just got a lot brighter! 🚀

#ActivityPub #fedidev #fediverse #opensource

가끔 생각하지만 Go에는 Result<T>와 삼항 연산자가 필요한게 아닌가 생각한다

if err != nil 이라는 반복적이고 예쁘지 않은 안티패턴들을 계속 만들어내게 된다

오히려 익명 함수같은 체계는 다른 언어보다 잘되어있고 더 직관적이라고 생각한다 익명 함수를 잘 활용할수 있는 환경에서도 없다는건 많이 아쉽다

TDD 실습으로 TDD의 한계점만 느끼고 있다. std::cin buffer를 바꿔치기해서 thread를 띄우고 gmock에 시간차를 두고 표준 입력을 전달하려니 이게 프로그램 테스트인지 C++ 지식 테스트인지 모르겠다. 테스트 코드가 테스트할 코드보다 어려운 현상은 매우 흔하며, 대개 src 폴더에 있는 코드보다 더욱 빠르게 레거시 코드로 상해버린다. 테스팅은 소프트웨어 개발 주기에서 필수적인 역할을 지니고 있으나 TDD가 프로그램의 명확함을 보장하는 방향으로 굴러가긴 어렵다. 명확한 프로그램은 선행되는 테스트가 아니라 명확한 설계에서 나오기 때문이다.

오늘의 짤

사랑하는 연합우주 가좍 여러분..
전할 말씀이 있습니다...

한국 연합우주 개발자 모임(https://fedidev.kr)이 파이콘 한국 2025에 커뮤니티 후원을 하게 되었는데요. 이를 통해 총 세 분께 이벤트로 파이콘 한국 2025 티켓을 드릴 수 있게 되었습니다..

파이콘 한국 2025에 참가하고 싶은 분들은!!! 이벤트에 응모해주시면 됩니다!!

[응모 자격]
연합우주 누구나

[응모 기한]
7월 27일 (일) 자정까지

[응모 방법]
이 글에 멘션으로 본인이 만든 페디버스 앱 자랑하기

개인이 사이드 프로젝트로 만든 mastodon/misskey/pixelfed 등등등 클라이언트,
액티비티펍 서비스의 API를 활용한 프로젝트(ex. quesdon)
액티비티펍 연동 라이브러리

등등등 어떤 것이든 좋습니다!!

--
응모하신 분 중 세 분을 선정하여 파이콘 한국 2025 티켓을 드리도록 하겠습니다.

많은 관심 부탁드려요~~

연합우주의 여러분을 파이콘 한국 2025에 초대합니다!

안녕하세요. Hackers' Pub이 이번 파이콘 한국 2025에 커뮤니티 후원을 하게 되었는데요. 이를 통해 총 세 분께 이벤트로 파이콘 한국 2025 티켓을 드릴 수 있게 되었습니다.

파이콘 한국 2025에 참가하고 싶었던 분들은, 이벤트에 응모해 주세요! 이벤트 응모 방법은 다음과 같습니다.

응모 자격

연합우주의 누구나

응모 기한

7월 27일(日) 자정까지

응모 방법

다음 주제어들 중 하나로 N행시를 멋지게 지어서, 인용 또는 답글로 달아주세요! (Mastodon의 경우에는 인용이 안 되므로 답글만 가능합니다.)

• 파이콘/파이컨
• 파이썬/파이선
• 해커스퍼브/해커즈퍼브/해커스펍/해커즈펍

예:

• 파이썬이 좋아서
• 이번에는 꼭 파이
• 콘에 가고 싶습니다!

응모하신 N행시 중 멋진 작품을 제출하신 세 분을 선정하여 파이콘 한국 2025 티켓을 드리도록 하겠습니다!

많은 참여 부탁드립니다!

https://github.com/bglgwyng/deferred-cleanup-resource-map 이런 라이브러리를 만들었다. ref counting 해서 GC 해주는 map인데, 해제를 임의로 늦출수 있다. LRU 캐시같은걸 일반화한 형태라고 보면 된다.

이름이 참 저질인데, 나도 upyo같은 센스있는 이름을 붙이고 싶었지만, 이게 클로드랑 머리맞대서 나온 최선이다;;

@tedpool테드풀 @kodingwarriorJaeyeol Lee @gaebalgom개발곰 @nyeongAn Nyeong (安寧) @joonnotnotJoon @crohasang크롸상 @z9mb1wwj @r4bb1t톡기 @2chanhaeng이찬행 @cosmic_elevatorSooji Choi @ooheunda @woaol벨 @meneleHanal Ae @devomdv @eottabom @hjleee93hyeonjeong lee 오늘 발대식에서 만나 뵈어서 반가웠습니다! 다시 한 번 앞으로 잘 부탁드립니다! 화이팅!

여성향 커미션 중개 플랫폼 크레페를 운영하는 쿠키플레이스에서 시니어 백엔드 엔지니어 채용을 진행중입니다. 채용공고에 해당 직무 소개, 복지, 연봉, 회사문화의 내용이 포함돼 있습니다. 많은 관심 부탁드립니다. Node.js, TypeScript, GraphQL에 대한 높은 숙련도 및 지식으로 팀에 기여해주실 분을 쿠키플레이스에서 극진히 기대하고 있습니다.

크레페에서는 이런 기술스택을 사용합니다

• Node.js, TypeScript, Vitest, Fastify
• GraphQL 　- Yoga, Relay, Pothos, Prisma
• ElasticSearch, MongoDB, FCM
• Docker, Github Actions
• AWS 　- ElasticBeanstalk, CloudWatch, Aurora PostgreSQL, Lambda, SES, S3, ElastiCache (Redis)
• Grafana, Sentry

구성원의 성장과 덕질을 지원해요

• 희망 도서 구매 (만화책 및 TRPG 룰북 포함)
• 워크샵 및 교육 프로그램 지원
• 전시, 공연 및 각종 행사 티켓 지원
• 월 5만 크레페 포인트
• 전동작탁 AMOS JP-EX COLOR
• 6인용 TRPG/보드게임 테이블

지원자님이 예상하실 수 있는 처우는 이래요

• 연봉: 최소 8000만원 ~ 최대 2억원 (주 40시간)
• 스톡옵션 부여에 열려있는 포지션

🎉 Huge shoutout to two amazing contributors from Korea's #OSSCA program who've made excellent contributions to #Fedify!

👏 @gaebalgom개발곰 tackled a tricky terminal compatibility issue in PR #282, fixing the fedify node command's favicon display on terminal emulators without truecolor support (#168). His solution elegantly detects terminal capabilities and falls back to 256-color mode when needed—ensuring a great experience across different environments.

🌟 @joonnotnotJoon enhanced Fedify's #WebFinger functionality in PR #281 by adding a configurable maxRedirection option to the lookupWebFinger() function (#248). He transformed a hardcoded limitation into a flexible, user-customizable parameter while maintaining perfect backward compatibility.

Both delivered thoughtful, well-implemented solutions that showcase the quality of contributions coming from the OSSCA program. Welcome to the Fedify community!

#ActivityPub #opensource #fedidev

@joonnotnotJoon 궁금해서 제 레포를 검색해보니 3년된 // FIXME: remove any가 있군요

내 블로그 글이 기상청 API 피해자 모임이래 ㅋ

오늘의 Zed 싱글벙글: Inlay Hint에 non-ASCII 텍스트가 있을 경우 Go to Definition하려고 커맨드 누른 채로 커서 올리면 에디터 전체 패닉 남