What is Hackers' Pub?

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.

5
0
0
0
0
0

Jaeyeol Lee shared the below article:

자기소개애

Eunsoo Eun @maxwell@hackers.pub

다양한 분야를 섭렵하며 '잡부'로 불리는 대학교 3학년 학생의 자기소개입니다. 커널 소스 분석, 리버싱 문제 풀이, AI 라이브러리 기여 등 폭넓은 활동을 하고 있으며, 러스트를 좋아하고 Haskell 학습을 희망하지만 게으름으로 미루고 있다는 솔직함이 돋보입니다. 대학원 진학을 꿈꾸지만 잦은 결석이 고민인 이 학생은, 다재다능함과 솔직한 매력으로 앞으로 어떤 활약을 보여줄지 기대감을 자아냅니다.

Read more →
15
0
0
SyoBoN @syobon@post.syobon.net
Public

世間が「Windows 11のUIがカス！」と言うなか「Windows 11めっちゃ良い」と言い、
世間が「iOS 26のUIがカス！」と言うなか「iOS 26めっちゃ良い」と言う人間
それがわたし
1
0
1

About

Juan @juanjin@hackers.pub

This post introduces Juan Jin, a programmer from South Korea with expertise in C, C++, Python, C#, and TypeScript. Jin's skills extend to platforms, libraries, and frameworks such as STM32CubeMX, ESP-IDF, FreeRTOS, Zephyr RTOS, and more. The author showcases personal projects like "Black Magic," a C macro metaprogramming research endeavor, and contributions to open-source projects like "Net for Dumbass" and "zpmgr." The post also details Jin's extensive work history, including roles at Bitbus, People-i, and other companies, where he developed diverse applications ranging from agricultural smart waterstream projects to military defense systems and IoT solutions. This overview highlights Jin's broad experience and technical capabilities, making it a valuable resource for those interested in embedded systems, IoT, and software development.

Read more →
5
0
0
0
0
0
0
0
0
2
1
0
1
0
0
1
0
0
SyoBoN @syobon@post.syobon.net
Public

「謎の半透明の板」じゃなくて「ガラス」と認識できるすりガラス風エフェクト、Windows Aero以来初めて見た
ありがとう、Liquid Glass
1
0
0
0
0
0
1
0
0
1
0
0
0
0
1
Phoronix @phoronix@masto.ai
Public

IO_uring Shows Promising Potential For Linux Accelerator Drivers

Last year there was some ideas raised around potentially making use of the Linux kernel's IO_uring functionality for graphics drivers to help with better performance and synchronization. It turns out Qualcomm engineers have recently been exploring IO_uring use for the DRM accelerator drivers with very promising results on their Cloud AI hardware in seeing around 50% spee…
phoronix.com/news/IO_uring-DRM

0
0
0

자기소개애

Eunsoo Eun @maxwell@hackers.pub

다양한 분야를 섭렵하며 '잡부'로 불리는 대학교 3학년 학생의 자기소개입니다. 커널 소스 분석, 리버싱 문제 풀이, AI 라이브러리 기여 등 폭넓은 활동을 하고 있으며, 러스트를 좋아하고 Haskell 학습을 희망하지만 게으름으로 미루고 있다는 솔직함이 돋보입니다. 대학원 진학을 꿈꾸지만 잦은 결석이 고민인 이 학생은, 다재다능함과 솔직한 매력으로 앞으로 어떤 활약을 보여줄지 기대감을 자아냅니다.

Read more →
15
0
0
0
0
0
0
0
0
0
0
0
7
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Are LLMs reliable translators of logical reasoning across lexically diversified contexts? ~ Qingchuan Li et als. arxiv.org/abs/2506.04575v1

arXiv logo

Are LLMs Reliable Translators of Logical Reasoning Across Lexically Diversified Contexts?

Neuro-symbolic approaches combining large language models (LLMs) with solvers excels in logical reasoning problems need long reasoning chains. In this paradigm, LLMs serve as translators, converting natural language reasoning problems into formal logic formulas. Then reliable symbolic solvers return correct solutions. Despite their success, we find that LLMs, as translators, struggle to handle lexical diversification, a common linguistic phenomenon, indicating that LLMs as logic translators are unreliable in real-world scenarios. Moreover, existing logical reasoning benchmarks lack lexical diversity, failing to challenge LLMs' ability to translate such text and thus obscuring this issue. In this work, we propose SCALe, a benchmark designed to address this significant gap through **logic-invariant lexical diversification**. By using LLMs to transform original benchmark datasets into lexically diversified but logically equivalent versions, we evaluate LLMs' ability to consistently map diverse expressions to uniform logical symbols on these new datasets. Experiments using SCALe further confirm that current LLMs exhibit deficiencies in this capability. Building directly on the deficiencies identified through our benchmark, we propose a new method, MenTaL, to address this limitation. This method guides LLMs to first construct a table unifying diverse expressions before performing translation. Applying MenTaL through in-context learning and supervised fine-tuning (SFT) significantly improves the performance of LLM translators on lexically diversified text. Our code is now available at https://github.com/wufeiwuwoshihua/LexicalDiver.

arxiv.org · arXiv.org

0
0
0
1
0
0
村上さん🔰 @AureoleArk@misskey.io
Public

うううううううううううううんきしょおおおおいい
なんかそんな予感はしてたんだけど、旧デザインのアプリと新デザインのアプリが同一画面に出てくるちぐはぐ感が完全にWindowsとか言うカスのOSみたいになってしまっている。

macOSはOSレベルでデザインを統一してくれていて美しいのが売りなのに、今回はほぼ吸収されていなくてゴミ

1
0
0
0
0
0
2
1
0
0
0
0
1
0
0
George Monbiot @georgemonbiot.bsky.social@bsky.brid.gy
Public

When did you ever hear the BBC stating that it must alter “story selection” and “other types of output, such as drama”, to win the trust of Green voters, or of unrepresented people on the left? All the shifts are in just one direction. bylinetimes.com/2025/06/09/b...

BBC Bosses Draw Up Plans to Wi...

BBC Bosses Draw Up Plans to Win Over Reform Voters by Changing News and Drama Output

The Director General Tim Davie and other executives discussed altering BBC “story selection” in order to secure the "trust" of supporters of Nigel Farage’s party

bylinetimes.com · Byline Times

0
0
0
0
0
0
1
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification. ~ Chengwu Liu et als. arxiv.org/abs/2506.04592v1

arXiv logo

Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification

Chain-of-Thought (CoT) prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs). However, to mitigate hallucinations in CoT that are notoriously difficult to detect, current methods such as process reward models (PRMs) or self-consistency operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness. To address this issue, we draw inspiration from the idea that "the gold standard for supporting a mathematical claim is to provide a proof". We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations. We evaluate our framework $Safe$ across multiple language models and various mathematical datasets, demonstrating a significant performance improvement while offering interpretable and verifiable evidence. We also propose $FormalStep$ as a benchmark for step correctness theorem proving with $30,809$ formal statements. To the best of our knowledge, our work represents the first endeavor to utilize formal mathematical language Lean 4 for verifying natural language content generated by LLMs, aligning with the reason why formal mathematical languages were created in the first place: to provide a robust foundation for hallucination-prone human-written proofs.

arxiv.org · arXiv.org

0
0
0
0
0
0
1
0
0
0
0
0
1
0
0
12
0
0
1
0
0
6
1
0
しろまだら @shiromadara@hackers.pub
Public
Shared by Perlmint

自己紹介の投稿を見かけたので、私も🥳

学生時代は生物学を学んでいましたが、手先が不器用で実験センスがなかったので、バイオインフォマティクスという分野で生物学のビッグデータ分析みたいなことをしていました🧬
長いこと大学などでスパコンを使って仕事をしていたので、民間企業に転職してからはモダンな開発の世界を知ることから始めています。
エンジニアのマネジメントをする立場ですが、自分が一番の初学者です。
Hackers’ Pubでも基本的なことを投稿すると思いますが、どうぞよろしくお願いします！

6
2
0
Jeff Atwood @codinghorror@infosec.exchange
Public
Shared by Jeff Atwood

@mdioneMarcos Dione this is pretty easy to demonstrate; I can generate a new email address that will get ZERO unwanted incoming emails, instantly, from a thousand different sources, and ten very reputable, widely and highly well regarded sources. How do I do that with a telephone number in the format (nnn) nnn-nnnn? Answer: I don't. No one does. No one EVER will, again, for the rest of recorded human history.

0
0
0
2
0
0
Linea @linea@hackers.pub
Public
Shared by Jaeyeol Lee

게임업계에서 기획하다 웹 프로그래머로 진로를 틀어보려 시도중입니다. 배운 과정들이 풀스택이라 백 프론트 다하고 있네요. 제가 생각해도 게임개발에서의 신입 TD 같은 기묘한 워딩같긴 한데 일단 전업해보려 노력중입니다 'ㅁ'/

영어, 일본어, 한국어 할 줄 알아요! 더 늘리고 싶지만 대충 언어 3개까지가 한계인 느낌이라 보류중!

5
1
0
1
0
0
2
0
0
1
0
0
RanolP @ranolp@hackers.pub
Public
Shared by Juntai Park

를 해볼까요.

  • @ranolpRanol☆P 와 동일인입니다...만 해당 계정은 근시일 내에 살릴 계획이 없습니다.
  • @ranolp 계정은 프로그래밍 언어론/해커스펍 사용기 위주 계정입니다.
  • 다시 말하자면 그 외 일상적인 내용은 트위터에서 이야기한다는 뜻입니다...
  • TypeScript와 얼추 호환되면서 제정신인 타입 추론 규칙을 가진 언어를 만들려고 타입 이론을 공부하고 있습니다.
    • 좀 많이 전에는 Bidirectional Typing (J. Dunfield, N. Krishnaswami)을 읽었었고,
    • 독일에 있는 튀빙겐 대학 내에서 연구하는 대수적 효과 언어 Effekt도 간단히 살펴보았었습니다.
    • 최근에는 힌들리-밀너-다마스 타입 추론 위에 얹은 부타입 확장을 살펴보고 있습니다.
      • 캠브릿지 대학 연구인 MLsub (S. Dolan and A. Mycroft)...
      • 을 단순화한 Simple-sub (L. Parreaux)을 시작으로 MLstruct, Ultimate Conditional Syntax 등 홍콩대 연구를 많이 보고 있습니다
      • MLscript가 정말 흥미로운 언어에요 ReScript but more Kotlin처럼 생겼음
  • 올해 들어서 An Infinitely Large Napkin으로 군론과 군의 작용, 위상수학과 대수 위상(호모토피만), 그리고 범주론을 배웠습니다.
  • 형식적 증명 보조기에도 관심이 많습니다.
    • Software Foundation을 통해 Coq (현 Rocq)를 약간 배웠습니다.
    • Lean 4도 약간 맛보기를 했습니다.
    • 의존 타입/마틴 뢰프 타입(MLTT)/호모토피 타입(HoTT) 등을 배워 간단한 증명 보조기도 만들어보고 싶네요.
      • 아마 An Infinitely Large Napkin 스터디가 끝나면 HoTT 스터디를 하지 않을까 싶네요.

15
0
0
0
0
0
bgl gwyng @bgl@hackers.pub
Public
Shared by Juntai Park

코딩중에 동작을 disable시키기 위해 주석을 많이 쓰는데, 이런것도 그냥 기본 문법에 Disable같은 키워드로 넣어 주면 좋겠다. 또 콘솔에 메시지를 찍을때 현재 소스 코드 위치를 찍는 것도 기본 기능으로 넣었으면 좋겠다.

이런 제안에 대해 거부감이 든다면(나도 듬), 그건 프로그래밍 언어의 문법이 완성된 코드라는 정적인 정보를 묘사하기 위함이라는 생각 때문일 거라고 짐작한다. 중간에 나오는 못난 코드들을 보조할 필요는 없다는 입장? 근데 사실은 못난 코드 보고 있는 시간이 코딩하는 시간의 99%다.

4
0
1
Sooji Choi @cosmic_elevator@hackers.pub
Public
Shared by Juntai Park

컴퓨터공학과 문화연구를 공부하고 있는 자유전공학부 학부생입니다! 아직 컴공 전공 수업을 듣지 못했지만, 2학기부터 수강하고 본격적으로 공부하기 시작할 예정입니다. 빅테크 기업의 인클로저와 자본 축적, 그로 인해 일어나는 노동착취를 비판적으로 바라보고, 그에 대항하는 정치적 실천으로서 기술의 가능성을 상상하고 있습니다. 일상과 정치 얘기는 @cosmic_elevator슥뽕귀신 , 독서 기록은 @exproot지수루트 에서 보실 수 있어요!

9
1
0