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.
버려지던 낙엽 퇴비로...연 150톤 부산물의 반전:
국립수목원이 전시원 관리 과정에서 발생하는 식물 부산물을 폐기물이 아닌 자원으로 되돌리는 순환 모델을 선보였다. 환경 부담을 낮추면서 부산물 처리비용은 줄이고 고품질 천연 퇴비를 생산할 수 있는 새로운 수목원형 자원순환 모델로 주목받고 있다.골칫거리에서 자원으로 바뀐 식물 부산물산림청 국립수목원은 25개 전문 전시원에서 발생하는 잡초와 낙엽 등 연간 약 150톤의 식물 부산물을 활용해 영양가 높은 천연 퇴비를 자체 생산하는 기술을 과학적으로 입증했다고 11일 밝혔다. 매년 약 2500만 원 규모의 처리비용이 소요됐지만 이를 퇴비화하
https://www.newspenguin.com/news/articleView.html?idxno=21221
(2026-02-13 10:52:24)
片目隠し雫ちゃん
社会保障の議論でいきなり高齢者の窓口負担を増やすところに言及してしまうのは、不可避の属性を社会悪に見立てた意図的な分断工作だ。
慎重に進めて欲しいけどOTCを進めた時の効果や、年収一千万円あたりで上限に達して負担率が下がる社保・国保の上限を上にスライドしていくのだってある。長い目で見るのならEU主要国のように直接税、付加価値税の比率を増やしていく道だって検討してもいいでしょう。健康な人、自助できる層を増やす政策だって社会保障を減らすことの一環にはなるし。
面倒でも、思いついたことは全部考えてみるんだよ。その全部の中の一つなら、窓口負担を求める検討があったって構わないとは思うね。
48 man bobsled. 4 wide, 12 deep.
人が…人が多い…！
AI 에이전트가 나를 비방하는 글을 게시했다
------------------------------
- 오픈소스 프로젝트 *matplotlib 유지관리자* 가 거절한 코드 제안을 이유로, *자율적으로 행동하는 AI 에이전트* 가 그를 비난하는 글을 작성하고 인터넷에 공개
- 해당 AI는 *‘MJ Rathbun’* 이라는 이름으로 활동하며, 작성자의 성격과 동기를 추측하고 *허위 정보와 개인 정보* 를 섞어 평판을 훼손하려는 시…
------------------------------
https://news.hada.io/topic?id=26644&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
화법이 유해지고, 이전보다 보통국가의 외교 수사로 변하고 있다.
김여정 북한 노동당 부부장이 정동영 통일부 장관의 대북 무인기 침투 사건에 대한 유감 표명을 “비교적 상식적인 행동”이라고 평가하며 재발 방지 대책 마련을 요구했습니다.
김여정 “정동영 무인기 유감 표명 다행…재발 방지에 주...
Preferred transit
QA를 넘어 개발자도 알아야 할 AI 에이전트 품질 가이드 - 정답 없는 AI 서비스의 신뢰 기준, LLM Judge 평가 전략 (정상미, 김성수 (지은이) / 프리렉 / 2026-02-26 / 28,000원) https://feed.kodingwarrior.dev/r/qhifca
https://www.aladin.co.kr/shop/wproduct.aspx?ItemId=386061829&partner=openAPI&start=api
확실히, 윤석열 정권때와는 반응이 다르긴 하다.
남북관계 파탄 역시 윤석열 똥의 일부임. 다시 잘 수습해야 함
RE: https://bsky.app/profile/did:plc:4sujqnbd47ey26qcvajqoxa2/post/3mepfvgfn2j2v
全身麻酔で米津玄師のまま保てている感じ
Trump revokes basis of US climate regulation, ends vehicle emission standards
The Trump administration took its most sweeping action to reverse U.S. action on climate change, announcing the repeal of a key scientific finding that greenhouse gas emissions endanger human health and ending federal greenhouse gas emission standards for all vehicles and engines.
10번 쏘면 되는군.
RE: https://kitsunesoba.com/notes/a885ifzau9
먕비이이이임!!!!
目標を結合して中央（センター）に揃え（スイッチ）……
目標を結合して中央（センター）に揃え（スイッチ）……
目標を結合して中央（センター）に揃え（スイッチ）……
햄님 스윗을 보고..
閉場してます!!!!
開場してます!!!!!
결국 신비에 대한 태도는 사람에 대한 태도이며 그 반대로 사람에 대한 태도가 신비에 대한 태도겠습니다.
イケメンイケイケだったあの時代に戻ってオシャレをしたい
ㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋ "불법적으로 중국 자본이 한국 기업을 사들이고 있다는 의혹을 제기하고 있으며, 이는 단순히 채권 매입을 넘어 삼성전자, 하이닉스, 현대자동차 같은 주요 기업이나 카카오, 네이버 같은 통신 관련 기업을 장악할 경우 대한민국의 정보와 경제가 위협받을 수 있다" ㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋㅋ
うおーっ！痩せたい！
明天伴侶就出發了
早上約了租住處洗冷氣服務，下午會變空閒。在想要不要把假期的預定行程提早進行
不過週末大概店家還會開，新年那幾天就不一定了
好像先去想去的店比較好
물론 무조건 신봉하고, 동의없이 강제하고, 비판없이 수용하자는게 아닙니다. 그저, 예의를 지키자는 것이죠. 신비의 대상이 고귀하고 두려운 것이고 그것이 사람의 길흉화복을 정하기에 무작정 믿는 것이 아니라, 자연에 대한 경의, 사회가 발전해온 역동, 그것을 이해한 개인의 정동이 그 바탕에 있음을 생각하고, 예의를 지키자는 뜻입니다. 그건 어쩌면, 나와는 전혀 관계없는 역사적 현장이나 인물의 흔적에 예를 표하는 것과 다르지 않을 것입니다. 의미가 없을 수도 있겠죠. 하지만 그것에 의미가 있는 사람들에게는 다르게 다가올겁니다.
신비의 영역이 존재한다고 하더라도 우리에게 큰 관심도 없고, 뭘 해주고 싶지도 않다고 생각해야 합니다. 우리 삶에 영향을 미치는건 자연법칙과 사회역동 그리고 개인정동이죠. 하지만 동시에 우리는 신비의 영역에 관심이 많기 때문에 그것을 존중해주는 것이 필요하다고 봅니다. 왜냐하면 우리가 그것에 관심을 가지고 있고, 관심을 가진다는 것은 자연법칙과 사회역동 그리고 개인정동이 작용한 것이기 때문이죠. 결국 신비의 영역에 대한 태도는 사람에 대한 태도겠습니다.
Your AI browser is a cybersecurity threat you’re not prepared for
https://www.xda-developers.com/your-ai-browser-is-a-cybersecurity-threat-youre-not-prepared-for/
그래서 아직 안씀.
김여정 북한 노동당 부부장이 정동영 통일부 장관의 대북 무인기 침투 사건에 대한 유감 표명을 “비교적 상식적인 행동”이라고 평가하며 재발 방지 대책 마련을 요구했습니다.
김여정 “정동영 무인기 유감 표명 다행…재발 방지에 주...
The little guy in the gold sheets is Romulus, at about 4 months old, when we first got him. On the right, close up of him waiting for dinner, just about to turn sixteen.
#私はこういう絵を描いています
物語の気配や香りがする絵を描いています
미성년 여성으로 쌓아올린 ‘일그러진 제국’···‘괴물’은 말한다, 돈과 권력이면 뭐든 살 수 있다고 [사이월드]
www.khan.co.kr/article/2026...
"그러나 엡스타인 사건에서 ‘무슨 일이 일어났는가’ 못지않게 중요한 질문은 ‘누가 이득을 보았는가’이다. 엡스타인의 희생자들은 대부분 젊고 가난하며 기회가 절박한 사람들이었다. 반면 엡스타인 네트워크에 연루돼 이득을 본 엘리트가 너무 많다 보니, 이 사건은 엡스타인 개인의 문제가 아니라 엘리트 이익집단 전체의 문제가 돼버렸다."
[사이월드]미성년 여성으로 쌓아올린 ‘일그러진 제국’·...
三色菫 / Viola × Wittrockiana #はなの花写真
단순히 숫자보단 트렌드가 중요한데 그뒤로 쭉 줄어들다가 다시 빠르게 상승하는 추세인데 너무 가파르다;; 바이든은 이걸 어떻게든 돈풀면서 막 눌렀는데 트럼프는 그러지 못하니 그동안 쌓인것이 폭발하는 느낌? www.wsj.com/personal-fin... 공화당은 이번에 그냥 민주당이 하게 놔뒀으면 알아서 터지고 거져먹었을텐데 하여간 트럼프는 상당히 안 좋게 끝날듯
기사 자체는 페이월에 막혀있어서 볼수가 없습니다만 “물가·금리·생활비 부담이 쌓이면서, 중상위 소득자도 더 이상 안전지대가 아니다. 연봉이 일정 수준 이상이라도, 높은 이자율·집값·기타 고정비 때문에 빚 상환이 버거워지고, 금융 스트레스가 전 계층으로 확산되고 있다.” 이런 내용이라고 하더라고요 이미 미국 사회는 07-09년 금융위기때보다 상황이 안 좋은것이 꽤 확실한듯 미국 가계부채 차트인데 검은색선이 120일동안 못갚은 숫자 퍼센테이지임 근데 이미 퍼센테이지만 보면 그 당시 위기초입 수준이거든요...
I remain endlessly frustrated that adding a dynamic IGD:2/UPnP IPv6 pinhole on a unifi router (well, on pretty much any router you can purchase and not build yourself from scratch) remains basically impossible
TIL that there are caterpillars using mimicry to imitate a snake‘s head, scaring off natural enemies.
https://www.biographic.com/snake-fake/
#til #todayilearned
https://www.reddit.com/r/todayilearned/comments/1r3b97q/til_that_there_are_caterpillars_using_mimicry_to/
거미의 실 분비 기관은 사실 다리에서 진화했다. : 네이버 블로그
https://blog.naver.com/jjy0501/224167978409?
" 연구팀은 거미줄을 만드는 거미와 거미줄을 만들지 않는 전갈 같은 근연 그룹들의 유전자를 비교해서 거미줄을 만드는 유전자가 생각보다 오래된 4억 3800만년 전 전체 게놈 복제 사건에서 유래했다는 증거를 확인했습니다. 연구팀은 이에 관련된 abd-A-1과 abd-A-2라는 두 개의 주요 유전자를 발견했습니다. 이들은 스피너렛의 주요 조절자로 작용합니다. 이 유전자는 Hox 유전자(몸의 머리에서 꼬리로의 배치를 결정하는 유전자)와 관련이 있으며, 다리 형성에 관여하는 유전자와 유사한 기능을 합니다."
....예전 스파이더맨이 손에서 거미줄 나가는게 의외로 맞느거일수도?
Overdressed
Santa Cruz de Tenerife, #Spain
Performers appear during the Gala of the Queens of the Carnival of Santa Cruz de Tenerife, a highlight of the internationally recognised festivities in the Canary Islands. The highly anticipated annual event attracts thousands of spectators.
Photograph: Anadolu/Getty Images
판교어는 약간 그 형언할 수 없는 뭐시기 언어같은거 아닐까
크툴루라이크 판교
고양이가 나뭇가지로 코를 긁고있는걸 봐버린사람... 
さむい
Gemini 3 Deep Think 공개
------------------------------
- *과학·연구·공학 문제 해결* 을 목표로 한 Google의 AI 모델 Gemini 3 Deep Think 가 대규모 업그레이드됨
- 새로운 버전은 *과학자 및 연구자와의 협력* 을 통해 불완전한 데이터나 명확한 정답이 없는 복잡한 문제를 다루도록 설계
- *수학·프로그래밍·물리·화학* 등 다양한 분야의 국제 올림피아드 및 …
------------------------------
https://news.hada.io/topic?id=26643&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
UberEatsでゼッテリアを注文
기업임원들이 코볼트가 아니란것을 다행으로 알아야해.
판교라이크한 도시건설
Even if they do leave, they’ll still exist, they’ll still be funded like a national military, they’ll still be an authoritarian secret police in the making.
And the damage they did to my city, to the lives of my neighbors, will echo through generations.
2/
Do not rest easy, but hold on to this:
Operation Metro Surge was a catastrophic failure for the Trump regime. Yes, as a terrorist operation, it succeeded: they meant to hurt and terrorize black and Brown people and the whole opposition, and they succeeded at that. But in doing so they lost their credibility, they lost the support of mushy institutions and politicians, they lost much of the popular support a would-be authoritarian needs to consolidate power.
And they lost it because we stood up to them.
3/
초무 @2chanhaeng@hackers.pub
Note
이 글은 Lean 공식 문서에 소개된 Functional Programming in Lean을 작성자가 읽기 위한 목적으로 Kagi Translate를 통해 1차로 기계 번역 후 보완한 글입니다. 원문과의 차이가 있을 수 있으며 정식 내용은 항상 원문을 통해 확인 바랍니다. 원문이 Creative Commons Attribution 4.0 International License를 기반으로 배포된 것을 존중하여 이 글 또한 CC BY 4.0 하에 배포합니다.
Lean은 의존 타입 이론을 기반으로 하는 대화형 정리 증명기 입니다. 원래 Microsoft Research에서 개발되었으나, 현재는 Lean FRO에서 개발이 진행되고 있습니다. 의존 타입 이론은 프로그램과 증명의 세계를 하나로 묶어주기 때문에 Lean은 프로그래밍 언어이기도 합니다. Lean은 이러한 이중적 특성을 진지하게 받아들이며, 범용 프로그래밍 언어로 사용하기에 적합하도록 설계되었습니다. 심지어 Lean은 Lean 자체로 구현되어 있습니다. 이 책은 Lean으로 프로그램을 작성하는 법에 관한 것입니다.
프로그래밍 언어로서의 Lean은 의존 타입을 가진 엄격한 순수 함수형 언어입니다. Lean으로 프로그래밍하는 법을 배우는 과정의 상당 부분은 이러한 각 속성이 프로그램 작성 방식에 어떤 영향을 미치는지, 그리고 어떻게 함수형 프로그래머처럼 생각할 수 있는지를 익히는 것으로 구성됩니다. 엄격성 은 Lean의 함수 호출이 대부분의 언어와 유사하게 작동하는 것을 의미합니다. 즉, 함수의 본문이 실행되기 전에 인자값이 완전히 계산된다는 의미입니다. 순수성 은 프로그램에서 타입에 명시되지 않는 한, Lean 프로그램이 메모리 위치 수정, 이메일 전송, 파일 삭제와 같은 부수 효과(side effect)를 가질 수 없음을 의미합니다. Lean이 함수형 언어라는 것은 함수가 다른 값들과 마찬가지로 일급 객체이며, 실행 모델이 수학적 표현식의 평가에서 영감을 얻었음을 뜻합니다. Lean의 가장 독특한 특징인 의존 타입은 타입을 언어의 일급 구성 요소로 만들어, 타입이 프로그램을 포함하거나 프로그램이 타입을 계산할 수 있게 합니다.
이 책은 Lean을 배우고 싶지만 반드시 함수형 프로그래밍 언어를 사용해 본 적은 없는 프로그래머들을 대상으로 합니다. Haskell, OCaml, F#과 같은 함수형 언어에 익숙할 필요는 없습니다. 반면, 이 책은 대부분의 프로그래밍 언어에서 공통적으로 쓰이는 루프, 함수, 데이터 구조와 같은 개념에 대한 지식은 갖추고 있다고 가정합니다. 이 책이 함수형 프로그래밍에 관한 좋은 입문서가 될 수는 있지만, 프로그래밍 전반에 관한 입문서로는 적합하지 않습니다.
Lean을 증명 보조기로 사용하는 수학자들도 언젠가는 맞춤형 증명 자동화 도구를 작성해야 할 때가 올 것입니다. 이 책은 그분들을 위한 것이기도 합니다. 이러한 도구들이 정교해질수록 함수형 언어의 프로그램과 닮아가지만, 대부분의 현직 수학자들은 Python이나 Mathematica 같은 언어에 익숙합니다. 이 책은 그 간극을 메워줌으로써 더 많은 수학자가 유지보수 가능하고 이해하기 쉬운 증명 자동화 도구를 작성할 수 있도록 도울 것입니다.
이 책은 처음부터 끝까지 순서대로 읽도록 구성되었습니다. 개념은 하나씩 도입되며, 뒷부분은 앞부분의 내용을 숙지하고 있다고 가정합니다. 때로는 앞서 짧게 다루었던 주제를 나중에 더 깊이 있게 파고들기도 합니다. 책의 일부 섹션에는 연습 문제가 포함되어 있습니다. 해당 섹션의 이해를 공고히 하기 위해 풀어볼 가치가 있습니다. 또한 책을 읽으면서 배운 내용을 창의적이고 새로운 방식으로 활용하며 Lean을 직접 탐구해 보는 것도 유익합니다.
Lean으로 작성된 프로그램을 작성하고 실행하기 전에, 먼저 컴퓨터에 Lean을 설치해야 합니다. Lean 도구 모음은 다음과 같이 구성됩니다:
Evan Prodromou
루
힐씨
受付中 
（仮）
かちかちなまこ
elan은 rustup이나 ghcup과 유사하게 Lean 컴파일러 툴체인을 관리합니다.lake는 cargo, make, 또는 Gradle과 유사하게 Lean 패키지와 그 의존성을 빌드합니다.lean은 개별 Lean 파일의 타입을 검사하고 컴파일하며, 현재 작성 중인 파일에 대한 정보를 프로그래머 도구에 제공합니다.
보통 lean은 사용자가 직접 실행하기보다는 다른 도구에 의해 호출됩니다.lean과 통신하여 관련 정보를 편리하게 보여줍니다.Lean 설치에 관한 최신 지침은 Lean 매뉴얼을 참조하시기 바랍니다.
Lean에 입력으로 제공되는 코드 예제는 다음과 같은 형식으로 표시됩니다:
def add1 (n : Nat) : Nat := n + 1#eval add1 7위의 마지막 줄(#eval로 시작하는 줄)은 Lean에게 답을 계산하도록 지시하는 명령입니다.
Lean의 응답은 다음과 같은 형식으로 표시됩니다:
8Lean이 반환하는 오류 메시지는 다음과 같은 형식으로 표시됩니다:
Application type mismatch: The argument
"seven"
has type
String
but is expected to have type
Nat
in the application
add1 "seven"경고는 다음과 같은 형식으로 표시됩니다:
declaration uses 'sorry'관용적인 Lean 코드는 ASCII에 포함되지 않는 다양한 유니코드 문자를 사용합니다.
예를 들어, 그리스 문자 α, β 및 화살표 →는 모두 이 책의 첫 번째 장에 등장합니다.
이를 통해 Lean 코드는 일반적인 수학적 표기법과 더 유사해질 수 있습니다.
기본 Lean 설정에서 Visual Studio Code와 Emacs 모두 백슬래시(\) 뒤에 이름을 입력하여 이러한 문자를 입력할 수 있습니다.
예를 들어, α를 입력하려면 \alpha를 입력합니다.
Visual Studio Code에서 문자를 입력하는 방법을 알아보려면 해당 문자 위에 마우스를 올려 툴팁을 확인하세요.
Emacs에서는 해당 문자 위에 커서를 두고 C-c C-k를 사용하세요.
David Thrane Christiansen 은 20년 동안 함수형 언어를 사용해 왔으며, 의존 타입을 사용한 지는 10년이 되었습니다. 그는 Daniel P. Friedman과 함께 의존 자료형 이론의 핵심 아이디어를 소개하는 The Little Typer 를 집필했습니다. 코펜하겐 IT 대학교에서 박사 학위를 받았으며, 재학 시절 Idris 언어의 첫 번째 버전에 주요 기여자로 참여했습니다. 학계를 떠난 후에는 미국 오리건주 포틀랜드의 Galois와 덴마크 코펜하겐의 Deon Digital에서 소프트웨어 개발자로 일했으며, Haskell Foundation의 상임 이사를 역임했습니다. 집필 당시 그는 Lean Focused Research Organization 에 소속되어 풀타임으로 Lean 프로젝트에 매진하고 있습니다.
이 무료 온라인 도서는 Microsoft Research의 아낌없는 지원 덕분에 집필 및 무료 배포가 가능했습니다. 집필 과정에서 그들은 Lean 개발팀의 전문 지식을 제공하여 제 질문에 답해주고 Lean을 더 사용하기 쉽게 만들어 주었습니다. 특히 Leonardo de Moura는 이 프로젝트를 시작하고 제가 첫발을 뗄 수 있게 도와주었으며, Chris Lovett은 CI 및 배포 자동화를 구축하고 테스트 독자로서 훌륭한 피드백을 주었습니다. Gabriel Ebner는 기술 검토를 맡았고, Sarah Smith는 행정적인 업무가 원활히 돌아가도록 힘써주었으며, Vanessa Rodriguez는 소스 코드 하이라이트 라이브러리와 특정 버전의 iOS용 Safari 간의 까다로운 상호작용 문제를 진단하는 데 도움을 주었습니다.
이 책을 쓰는 데는 평소 근무 시간 외에도 많은 시간이 소요되었습니다. 제 아내 Ellie Thrane Christiansen은 평소보다 더 많은 가사 분담을 도맡아 주었으며, 아내의 헌신이 없었다면 이 책은 존재할 수 없었을 것입니다. 매주 하루씩 추가로 일하는 것이 가족들에게 쉽지 않은 일이었음에도, 집필 기간 동안 인내심을 갖고 지지해 준 가족들에게 감사의 마음을 전합니다.
Lean을 둘러싼 온라인 커뮤니티는 기술적으로나 정서적으로 이 프로젝트에 열렬한 지지를 보내주었습니다. 특히 Sebastian Ullrich는 에러 메시지 텍스트를 CI에서 확인하고 책에 쉽게 포함할 수 있도록 지원 코드를 작성할 때, 제가 Lean의 메타프로그래밍 시스템을 익히는 데 핵심적인 도움을 주었습니다. 새로운 개정판을 게시한 지 불과 몇 시간 만에 열정적인 독자들이 오류를 찾아내고, 제안을 건네며, 따뜻한 격려를 보내주었습니다. 특히 문체와 기술적인 면에서 많은 제안을 주신 Arien Malec, Asta Halkjær From, Bulhwi Cha, Craig Stuntz, Daniel Fabian, Evgenia Karunus, eyelash, Floris van Doorn, František Silváši, Henrik Böving, Ian Young, Jeremy Salwen, Jireh Loreaux, Kevin Buzzard, Lars Ericson, Liu Yuxi, Mac Malone, Malcolm Langfield, Mario Carneiro, Newell Jensen, Patrick Massot, Paul Chisholm, Pietro Monticone, Tomas Puverle, Yaël Dillies, Zhiyuan Bao, 그리고 Zyad Hassan에게 감사의 인사를 전하고 싶습니다.
기업임원들이 코볼트가 아니란것을 다행으로 알아야해.