Hackers' Pub is a place for software engineers to share their knowledge and experience with each other. It's also an ActivityPub-enabled social network, so you can follow your favorite hackers in the fediverse and get their latest posts in your feed.
デイリーポータルZ @dailyportalz.jp@web.brid.gy
服を買うときに「ちょっとしたパーティーにも着ていけますよ」と言われることがある。デイリーポータルZを読んでいるみなさんとその「ちょっとしたパーティー」を一緒に開催することになった。
デイリーポータルZ @dailyportalz.jp@web.brid.gy
見た目はかわいいものの、お値段がかわいくないシルバニアファミリー。容易に買えない、でも娘には遊ばせてあげたい。そうだ、作っちゃおう！
かえりたい
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
いつからトランプが2期で大統領をやめると勘違いしていた？ #こわい考えになってしまった
是台股在震嗎 
게임 프로그래밍에서 AI에 대한 John Carmack의 견해
------------------------------
- Microsoft가 AI로 생성된 Quake II 데모를 공개한 것에 대한 비판(개발자의 가치를 훼손한다는 주장)에 대한 반론
- Doom/Quake의 개발자 존 카맥은 AI가 개발자, 아티스트, 디자이너의 기술을 폄하한다는 주장을 이해하며 이에 대한 본인의 생각을 정리
# 기술의 진보는 불가피한 변화임
- 과거에는 …
------------------------------
https://news.hada.io/topic?id=20223&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
결국 VOD 나왔구나 ㅠㅠ
미키 17 - Apple TV (KR) https://tv.apple.com/kr/movie/%E1%84%86%E1%85%B5%E1%84%8F%E1%85%B5-17/umc.cmc.4sy8d2jaavdrnbbyh56dao7nf
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
[Git turns 20: A Q&A with Linus Torvalds - The GitHub Blog](https://github.blog/open-source/git/git-turns-20-a-qa-with-linus-torvalds/)
//Linux Torvalds創造Git，很像Donald Knuth創造TeX。兩人都是為了自己心愛的計畫創造一個工具來解決他不滿的問題（Linus是版本控制軟體，Knuth是電腦排版），然後這兩個工具都永遠留在自由軟體的地景上。（古典）文學上有種說法，巨擘的盛宴掉下來的一點菜渣就足以養活整個世代的心靈，軟體世界似乎也是這樣。
Living in the United States these days is looking around and repeating "It didn't have to be this way" over and over and over again.
하.. S3는 글로벌하게 네임스페이스를 구분하지 않았으면 좋겠다... 이름 짓기 너무 힘들다ㅠ.ㅠ.
“응원봉 광장이 내 삶을 바꿨다” 노조·정당 가입하는 2030 여성·성소수자
수정 2025-04-09 07:26 www.hani.co.kr/arti/society...
“응원봉 광장이 내 삶을 바꿨다” 노조·정당 가입하는 ...
Anyone want a free Duratech soldering station? I don't use it any more since buying a Pinecil. DM me if you're interested, pickup from Belgrave, VIC or nearby suburbs.
相変わらず発言が無責任すぎて笑う / 「AppleはiPhoneを米国内で製造できる」──トランプ政権 - ITmedia NEWS https://www.itmedia.co.jp/news/articles/2504/09/news107.html
老梗笑話，但一直很萬用啊～
第1任因為對方外遇而離婚，第2任則是因為對方負債太多而離婚。但就算如此,我弟弟(39歳)還想要再婚。我嚇到了，覺得真的假的啦。
於是我老爸(72歳)說了『人啊，因為“判斷力不足”而結婚，因為“忍耐力不足”而離婚，又因為“記憶力不足”而再婚』這樣的名言。
果然是人生結過3次婚的老前輩才能說出的響亮話語。
---
最近又看到有影片演出這一段...
新技術を前にしてこれって危なくないですか？と指摘することは誰でもできるけど、それを検討してどう使うとリスク減らして有益に使えるかを考えられる人は限られている印象
うりうりのうりう
윤석열 대선 캠프의 첫 대변인을 맡았던 이동훈 전 조선일보 논설위원이 윤석열의 김건희에 대한 감정은 ‘사랑 이상’이라고 설명했습니다. 읽기 조금 버거운 기사입니다.
“윤, 김건희가 면박주는데 강아지 안고 웃기만” 윤캠 ...
うちの犬の写真擬人化して、って投げたらすごいの返ってきた。そうじゃないねんｗ
技術的には可能ですが流れてきた
@ailrunAilrun (UTC-5/-4) 재밌게 잘 읽었습니다. 걱정하신 것과 다르게 저에게는 쓰신 글이 술술(?) 잘 읽혔어요. 이제 다음 글은 Dependent Haskell인가요!
@curry박준규 Dependent Haskell은 흥미로운 내용을 다루기에는 아직 너무 갈 길이 멀고... 그렇다고 동기만 다루자니 좀 심심하네요. 아마 Agda나 Coq등을 조금 다뤄보지 않을까 싶습니다. 관련 내용으로 Dependent Haskell을 좀 언급할 수는 있겠습니다.
코딩 에이전트 구축을 위해 LangGraph를 선택한 이유
------------------------------
- Qodo는 GPT-3 시절부터 AI 코딩 보조 도구를 개발해온 팀으로, 최근에는 더 유연하고 동적인 코딩 에이전트를 만들기 위해 LangGraph 프레임워크를 선택
- 이 문서는 LangGraph가 어떻게 개발 흐름의 유연성과 코드 품질 기준을 동시에 만족시킬 수 있었는지를 설명함
# 초기 구조적 접근 방식에서 LangGraph로…
------------------------------
https://news.hada.io/topic?id=20220&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
린스: 삭제됨
샴푸: 평범함
바디워시: 동위원소 연대측정이 불가능해질때까지 남아있음
Hey I'm still looking for work.
I've applied to a lot of places in my area and I'm getting nothing.
I'm a programmer at heart, but I've also been looking for regular entry-level jobs because there haven't been any coding positions open at my level as far as I could tell.
If you can offer me a job, it might save my butt. And if you can't offer me a job, could you at least share this post?
I live 30 minutes away from Bellevue if that helps.
#fedihire #getfedihired #programmerforhire #programmer4hire #coderforhire #coder4hire #lookingforwork #looking4work #unemployed #pleasehireme #java #kotlin #scala #c #cplusplus #csharp #dotnet #zig #godot #godotengine #gdscript
まちゅ
15歳でデビューした少年が、その爆発的な人気にむしろ追い詰められ心を破壊されていく映画(ベターマン)を見たばかりなので、広末が早稲田入学したときの映像を見て「大人気だったのに落ちぶれて」とは全然思えない。むしろこういう人気のあり方こそが彼女を壊していったんじゃないの。知らんけど。
16歳でブレイク後、人気絶頂だった広末がなぜ大学に進学したか。少しでも"ふうーの社会"と接点を持ち、"ふうーの人間"でいられる時間を作りたかったのだとしたら。それなのに大学側は守ってくれず、むしろ宣伝に利用するような態度で、群衆の歓声とメディアスクラムに囲まれた初登校。私だったら絶望するな。芸能人じゃない自分でいることは許されないと突き付けられるようなものでしょ。広末がどう感じたかは知らんけど。
そして今、中居と違って彼女を決死援護してくれるファンはいない。"かわいいだけでチヤホヤされてた女"が破綻していくのを嬉々として眺める連中ばかり。広末の"奇行"よりそっちのがよっぽど邪悪だよ。
해커스펍을 스마트해지기 위한 용도로 쓰고 있다. 대수롭지 않은 생각도 어디안쓰면 쓸데없이 머릿속에서 리플레이된다. flush를 자주 하자...
RE: https://social.silicon.moe/@realgsong/114300412588845941
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
洪 民憙 (Hong Minhee) shared the below article:
Ailrun (UTC-5/-4) @ailrun@hackers.pub
국밥 두 그릇의 가격이 얼마인가? KTX의 속력이 몇 km/h인가? 내일 기온은 몇 도인가? 일상에서 묻는 이런 질문은 항상 같음의 개념을 암시적으로 사용하고 있다. 앞의 예시를 보다 명시적으로 바꾼다면 아래와 같이 (다소 어색하게) 말할 수 있다.
이런 질문들의 추상화인 이론들은 자연스럽게 언제 무엇과 무엇이 같은지에 대해서 답하는 데에 초점을 맞추게 된다. 예를 들면
등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,
이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aa와 bb를 입력으로 주었을 때
알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aa와 bb에 대해 aa와 bb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.
이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aa와 bb에 대해 aa와 bb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.[1]
그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.
이 방법은 말 그대로 두 프로그램이 문법 수준에서 같은지를 보는 것이다. 예를 들어 다음의 두 JavaScript 프로그램은 문법적으로 같은 프로그램이다.
くろでん
Alternative_Talk 
lionhairdino
しゅいろ
악하// 1번 프로그램
let x = 5;
console.log(x);
// 2번 프로그램
let x = 5;
console.log( x );공백문자의 사용에서 차이가 있으나, 그 외의 문법 요소는 모두 동일함에 유의하자. 반면 다음의 두 JavaScript 프로그램은 동일한 행동을 하지만 문법적으로는 다른 프로그램이다.
// 1번 프로그램
let x = 5;
console.log(x);
// 2번 프로그램
let x = 3 + 2;
console.log(x);두 프로그램 모두 x에 5라는 값을 할당하고 5를 콘솔에 출력하나, 첫번째 프로그램은 = 5;를, 두번째 프로그램은 = 3 + 2을 사용하여 5를 할당하고 있기 때문에 문법적으로 다르다.
문법적 비교는 이렇게 문법만 보고서 쉽게 판정할 수 있다는 장점이 있으나, 두번째 예시처럼 쉽게 같은 행동을 함을 이해할 수 있는 프로그램에 대해서도 "같지 않음"이라는 결과를 준다는 단점을 가진다. 혹자는
3 + 2같은 계산은 그냥 한 다음에 비교하면 안돼? 컴파일러(Compiler)도 상수 전파(Constant Propagation) 최적화라던지로3 + 2를5로 바꾸잖아?
라는 생각을 할 수도 있을 것이다. 이 제안을 반영한 방법이 바로 β\beta 동등성이다.
바로 앞의 소절에서 단순 계산의 추가에 의해 같음이 같지 않음으로 변하는 것을 보았다. 이런 상황을 피하기 위해서는 같음을 평가할 때 프로그램의 실행을 고려하도록 만들어야 한다. 가장 대표적인, 대부분의 프로그래밍 언어(Programming Language)에 존재하는 프로그램의 실행은 함수 호출이다. 따라서 함수 호출을 고려한 같음의 비교는 f(c)와 함수 f의 몸체 b 안에서 인자 x를 c로 치환한 것을 같다고 취급해야한다. 예를 들어
let f = (x) => x + 3;이 있다면, f(5)와 5 + 3 혹은 8을 같은 프로그램으로 취급해야한다. 이 비교 방법의 큰 문제는 함수가 종료하는지 알지 못한다는 것이다. 두 프로그램 a와 b를 비교하는데, a가 종료하지 않는 함수 l을 호출한다면, 이 알고리즘은 "같음"이나 "같지 않음"이라는 결과를 낼 수조차 없다. 즉, 올바른 판정법이 될 수 없다.
더 심각한 문제는 아직 값을 모르는 변수가 있는 "열린 프로그램"("Open Program")에 대해서도 이런 계산을 고려해야한다는 것이다. 다음의 JavaScript 예시를 보자.
let g = (x) => f(x) + 3;
let h = (x) => (x + 3) + 3;g와 h는 같은 프로그램일까? 우리가 g와 h가 같은 프로그램이기를 원한다면 f(x)와 x + 3을 같은 프로그램으로 보아야한다. 대부분의 프로그램은 함수 안에서 쓰여지기 때문에 프로그램의 비교는 거의 항상 g와 h의 몸체와 같은 열린 프로그램들의 비교이다. 따라서 g와 h를 다른 프로그램으로 본다면 계산을 실행하여 두 프로그램을 비교하는 의미가 퇴색되고 만다. 그렇기 때문에 우리는 x와 같이 값이 정해지지 않은 변수가 있을 때에도 f(x)을 호출하여 비교해야만 한다. 이는 우리가 단순히 모든 함수가 종료하는지 여부를 떠나서, 함수의 몸체에 등장하는 모든 부속 프로그램(Sub-program)이 종료하는지 아닌지를 따져야만 한다는 이야기이다.
이런 강한 제약조건으로 인해 β\beta 동등성을 통해서 프로그램 비교의 판정 문제를 해결 가능한 곳은 매우 제한적이지만, β\beta 동등성이 매우 유용한 한가지 경우가 있다. 바로 의존 형이론(Dependent Type Theory)의 형검사(Type Checking)이다.
의존 형이론은 형(Type)에 임의의 프로그램을 포함할 수 있도록 하는 형이론(Type Theory)의 한 종류이다. 예를 들어 명시적인 길이(n)를 포함한 벡터(Vector) 형을 Vector n Int과 같이 쓸 수 있다. 이 형은 n개의 Int값을 가진 벡터를 표현하는 형이다. 이제 append라는 두 벡터를 하나로 연결하는 함수를 만든다고 해보자. 대략 다음과 같은 형을 쓸 수 있을 것이다.
append : Vector n a -> Vector m a -> Vector (n + m) a즉, append는 길이 n짜리 a 형의 벡터와 길이 m짜리 a 형의 벡터를 합쳐서 길이 n + m짜리 a 형의 벡터를 만드는 함수이다. 이 함수를 사용해서 길이 5의 벡터를 길이 2와 길이 3짜리 벡터 x, y로부터 만들고 싶다고 하자.
append x y : Vector (2 + 3) a안타깝게도 우리는 길이 2 + 3짜리 벡터를 얻었지, 길이 5짜리 벡터를 얻진 못했다. 여기서 앞서의 질문이 다시 돌아온다.
아니,
2 + 3를5로 계산하면 되잖아?"
그렇다. 이런 의존 형에 β\beta 동등성을 적용하면 우리가 원하는 형을 바로 얻어낼 수 있다. Vector (2 + 3) a과 Vector 5 a는 같은 형이기 때문이다. 더욱이, 의존 형의 경우 종료하지 않는 부속 프로그램이 잘못된 형을 줄 수 있기 때문에 많은 경우 종료하지 않는 부속 프로그램을 어차피 포함하지 않는다. 다시 말해, 앞서 말한 제약 조건 즉 모든 부속 프로그램이 종료해야만 한다는 제약조건은 의존 형의 경우 상대적으로 훨씬 덜 심각한 제약조건이 되는 것이다.
이런 의존 형에 있어서의 β\beta 동등성 검사를 "변환 검사"("Conversion Check")라고 하며, 두 형이 β\beta 동등일 경우 이 두 형이 서로 "변환 가능하다"("Convertible")라고 한다. 이 변환 검사는 의존 형이론 구현에 있어서 가장 핵심인 기능 중 하나이며, 가장 잦은 버그를 부르는 기능 중 하나이기도 하다.
이 글에서는 같음과 같지 않음의 판정 문제에 대해 간략히 설명하고 프로그램의 같음을 판정하는 법에 대해서 단순화하여 다루어보았다. 구체적으로는 문법 기반의 비교와 β\beta 동등성을 통한 비교로 프로그램의 같음을 판정하는 법을 알아보았고, 이 중 β\beta 동등성이 적용되는 가장 중요한 예시인 의존 형이론을 β\beta 동등성을 중점으로 짤막하게 설명하였다. 마지막 문단에서 언급했듯 의존 형이론의 구현에 있어서 β\beta 동등성을 올바르게 구현하는 것은 가장 중요한 작업 중 하나이기에, 최근 연구들은 β\beta 동등성의 구현 자체를 의존 형이론 안에서 함으로서 검증된 β\beta 동등성의 구현을 하기 시작하고 있다. 이 글이 같음과 같지 않음과 판정 문제 그리고 β\beta 동등성에 있어 유용한 설명을 내놓았기를 바라며 이만 줄이도록 하겠다.
두 함수가 같다라고 보는 방법에 따라 다르나, 두 함수가 항상 같은 값을 가진다면 같다고 하자. 이때 함수의 판정 문제는 정지 문제(Halting Problem)와 동일하다. 임의의 튜링 기계(Turing Machine) ff가 입력 nn을 받았을 때 종료하면 g(n)=1g(n) = 1, 아니면 g(n)=0g(n) = 0이라고 하면 이 함수 gg와 상수 함수 c(n)=1c(n) = 1가 같은 함수임을 보이는 것은 ff가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
Git 20주년 회고 – 여전히 이상하고, 여전히 멋진 도구
------------------------------
- Git은 20년 전 Linus Torvalds가 첫 커밋을 하며 시작된 버전 관리 시스템임
- 원래는 단순한 개인 프로젝트였지만, 이후 전 세계적으로 가장 널리 사용되는 버전 관리 시스템으로 성장함
- 작성자는 GitHub 공동 창립자이며, Git 관련 책과 커뮤니티를 구축하면서 Git의 발전에 깊게 관여해왔음
- 초기에는 단…
------------------------------
https://news.hada.io/topic?id=20217&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
Avvy라는, 약건 픽크루 같은 느낌의? 무료 버츄얼 앱인데 이런느낌으로 인식되는구나~ 같은걸 해볼 수 있어서 재밌네요...
OBS로 영상을 보낼수도 있는 것 같아요
Greenland
라이프넷으로 샴푸 린스(는 다써서 새로 사야됨) 바디워시 세 개 다 맞춰서 쓰고 있어요
바디워시 추천 받아요
"진보는 분열로 망한다"는 레토릭이 있는데, 왜 분열하면서도 승리할 수 없다고 생각하지? 반대로 왜 수구세력은 분열될 수 없다고 생각하지? 이 말 자체부터가 교묘한 프레임이라고 생각함.
I dont like “-gate”. Could we go back to using “The ___ affair”? Sounds more mysterious.
Jira, Linear 등 일정 관리 앱이 풀어야할 가장 어려운 문제는, 사용자 중 상당수는 애초에 일정 관리를 하기 싫어하는 사람이라는 것이다. 안타깝게도 나도 거기 포함되는데, 문제는 그런 사람일 수록 일정 관리가 꼭 필요하다. 나중에 프로젝트가 복잡해지면 일정 관리 앱을 켜는 거 자체를 꺼리게 된다. 이걸 어쩌면 좋지.
ねむ…
How Netflix Accurately Attributes eBPF Flow Logs
Link: https://netflixtechblog.com/how-netflix-accurately-attributes-ebpf-flow-logs-afe6d644a3bc
Discussion: https://news.ycombinator.com/item?id=43624888
제 이동 수단은
트렉스타. 고어텍스. 보아. 하이퍼그립.
Hyperlight WASM: 빠르고, 안전하고 OS-Free
------------------------------
- Hyperlight Wasm은 Microsoft가 CNCF에 기부한 *초경량 가상 머신(VM)* 기술 Hyperlight의 최신 확장 버전으로, * WebAssembly(Component Model 기반)* 워크로드를 빠르고 안전하게 실행함
- 전통적인 VM과 달리 OS나 가상 디바이스 없이 *메모리 슬라이스와 CPU만 노출* , 1~2ms의 빠른 부팅 시간 제공
- 다양…
------------------------------
https://news.hada.io/topic?id=20219&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
AndroidのChromeはバックグラウンドになるとWebSocketを閉じるっぽい。そっかー。
슈커퍼브 사고 싶다
크아악 커브 이쁘다
CW의 민감도에 대한건 사람마다 다르고 그 적당한 범위는 사람마다 다를 수 밖에 없잖아..
이게 센서등이랑 비슷하다고 보는데, 자동 센서등은 정말 '알잘딱'하게 적당한 민감도로 불을 켜줘야 편한 물건이잖아요. 거실에서 움직이고 있는데 현관 센서등이 켜지면 너무나 불편하고, 센서등으로서 역할을 못하고 있다고 생각하게 되죠. CW도 마찬가지라 봅니다.
그게 누구라도 자기가 생각하는 민감도와 다른 사람을 못견뎌하는 사람을 전부 다 배려하는건 불가능하구요. 도저히 못 견디겠으면 자신의 타임라인을 자기가 생각하는 정규 분포에 가까운 사람들로만 채우는걸 추천드립니다..
우리의 가장 분열된 목소리가 적들의 가장 단결한 악바리를 압도하는 날이 오기를 바라며 투쟁.
Jake Hamilton
박준규
