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.
ねれてない
にゃあああ
There should be a version of the Radiohead song Creep but it’s about being Normal
Huh, The Onion used to have a semi-real dating site.
https://web.archive.org/web/20070315065255/http://personals.theonion.com/
Discord has taken a bold new strategy of regularly playing notification pings but never highlighting any kind of message. I think it's just lonely, which is understandable
this new discord update is awful
@lynnesbianLynnesbian 
these tariffs are getting ridiculous
#wildlife #nature #birds #picnickingbirds
Picnicking Birds 🪶
Mistakes and cool things to do with arena allocators https://lobste.rs/s/3lf0w3 #programming
https://zylinski.se/posts/dynamic-arrays-and-arenas/
if you know, you know
Hi
Hey Fedi fam? If I enjoyed games like Fallout 3 and 4, and Skyrim, will I have decent odds of enjoying Red Dead Redemption 2?
I can get it for $15 on Steam right now, seriously considering it. I owned it once, but found it required me to create a Rockstar games account, I hate that shit. But it does look like a lot of fun.
되게 극단적인 법안인데, 몬타나 주에서는 트랜스젠더 아동의 부모를 중범죄로 처벌하는 법안이 발의되었습니다. 트랜스젠더 아동에게 맞는 약물을 처방받은 것만으로 부모와 의사를 중범죄로 처벌 수 있다는 내용인데요. 논바이너리 의원의 열띤 연설과 양심을 가진 18명의 공화당 의원들의 반대로 결국 해당 법안은 폐기되었습니다!🏳️⚧️ 승리입니다!!!
아래의 타래는 생중계 타래입니다.
RE: https://bsky.app/profile/did:plc:m65ifh7vn5zdgs7izcmht4gy/post/3lmd63hicss24
'트랜스젠더 청소년들은 정체성이 확립이 안되어서 약물투여를 하면 안된다!' 라는 혐오자의 주장에 반대하며 그래서 2차성징을 늦추는 약물(puberty blocker)을 투여하며, 트랜지션을 해도 되냐 아니냐가 정해졌을 때 그 약물 투여를 중단/HRT를 시작하여 정할 수 있게 합니다. 그냥 막 놔주는 거 아니에요. 좀 혐오자 니놈들은 생각을 쳐 하고 글을 싸기를 바랍니다. 또 puberty blocker는 청소년들에게 해롭다고 언론플레이 되어있지만, 정작 성조숙증을 겪고 있는 청소년들에게는 잘만 처방됩니다. 선택적 해로움인가요?
You can press Ctrl-L while in the shell to clear the screen.
Gary has published a new video on his 5 top tips for home labbers, focusing on pfSense/opnsense. Like always, good tips for those of us who are using these filters in their network. Thanks 
@garyhtech !
104%
의료 하니까 또 불합리한 것이 생각났는데... 보통 가슴 수술은 아래와 같이 구분됩니다. 1. 여유증 시스젠더 남성의 적출 치료 2. 시스젠더 여성의 미용 목적 확대 치료 3. 시스젠더 여성의 삶의 질 개선 목적 축소 치료 4. 트랜스젠더 여성 범주의 트랜지션 목적 확대 치료 5. 트랜스젠더 남성 범주의 트랜지션 목적 적출 치료 하지만 이러한 치료들 중에서도 간극이 존재하는데요 왜냐면... 이 중에서 의료보험을 받을 수 있는 것은 1번 뿐입니다.... 1번이 꼭 필요하다고 한다면, 3, 4, 5번도 꼭 필요한 것인데 말이죠.
how it started: how it's going: (jj new lv + fix one line conflict + jj squash) #jj-vcs
'트랜스젠더 청소년들은 정체성이 확립이 안되어서 약물투여를 하면 안된다!' 라는 혐오자의 주장에 반대하며 그래서 2차성징을 늦추는 약물(puberty blocker)을 투여하며, 트랜지션을 해도 되냐 아니냐가 정해졌을 때 그 약물 투여를 중단/HRT를 시작하여 정할 수 있게 합니다. 그냥 막 놔주는 거 아니에요. 좀 혐오자 니놈들은 생각을 쳐 하고 글을 싸기를 바랍니다. 또 puberty blocker는 청소년들에게 해롭다고 언론플레이 되어있지만, 정작 성조숙증을 겪고 있는 청소년들에게는 잘만 처방됩니다. 선택적 해로움인가요?
박준규 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 프로그램은 문법적으로 같은 프로그램이다.
くろでん
arc) 
Stefano Marinelli
// 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가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎
oh that's fun, many people put a lot of effort to make obscure software packages reproducible but apparently one of the most important security tools in the world isn't https://github.com/signalapp/Signal-iOS/issues/641
되게 극단적인 법안인데, 몬타나 주에서는 트랜스젠더 아동의 부모를 중범죄로 처벌하는 법안이 발의되었습니다. 트랜스젠더 아동에게 맞는 약물을 처방받은 것만으로 부모와 의사를 중범죄로 처벌 수 있다는 내용인데요. 논바이너리 의원의 열띤 연설과 양심을 가진 18명의 공화당 의원들의 반대로 결국 해당 법안은 폐기되었습니다!🏳️⚧️ 승리입니다!!!
아래의 타래는 생중계 타래입니다.
RE: https://bsky.app/profile/did:plc:m65ifh7vn5zdgs7izcmht4gy/post/3lmd63hicss24
Because of the ongoing fucktastrophe, the cries of "Use SIGNAL!" are constant and unavoidable. And I get it, it may be the least-bad option in a sea of terrible options. If, that is, you choose to ignore the advice of "don't use your phone for that shit" (the Stringer Bell Rule).
But out of curiosity, because I haven't been keeping up, has the Signal Corporation addressed: ...
A shot from November last year that I somehow never shared.
📷 Pentax 6x7
🎞️ Kodak Portra 160
🔭 Super Takumar 105mm/2.4
👤 
@AmeboidAmelia Rochko
⚗ Spieker Film Lab
#BelieveInFilm #FilmPhotography #AnalogPhotography #MediumFormat
OH: "Bei Code-Signing ist es glaub wichtig, dass man den private key nicht kennt' - 'Das kann man so oder so sehen'
#nixdaleaks
does anyone have tips for setting up a colourscheme in the shell that doesn't have some horrible clash in it somewhere? I'm trying to write down advice but personally my approach has been "just use Solarized Light & accept that some things will look bad occasionally” and that doesn't seem great (some "bad" things in the screenshots)
curious to hear anything that's worked for you! The only thing I know of that seems useful is the "minimum contrast" feature some terminal emulators have
Netbird: connect your devices into a WireGuard overlay network with SSO, MFA and granular access controls via 
@fanfTony Finch https://lobste.rs/s/tfeskt #networking #security
https://github.com/netbirdio/netbird
The SRE regular-expression notation (1998) https://lobste.rs/s/bn0m18 #lisp #plt
https://www.khoury.northeastern.edu/~shivers/papers/sre.txt
xan is a CLI tool that reads & displays visualizations from CSV files in the terminal.
It features shell tab completion, parallel processing, filtering, sorting, and previewing CSV data in histograms, tables, heatmaps and more.
medialab (medialab on GitHub) made xan & is Terminal Tool of the Week! ⭐️
Just committed OpenSSL 3.5.0 release to FreeBSD ports.
New LTS. Hope this is added to FreeBSD 15!
This tiny thorn caused me a #puncture today.
Thankfully, I am #prepared for this inevitability and always carry a toolkit and a spare tube inside the frame of my #brompton, aswell as a pump on the frame.
(I love how neatly all of that packs.)
I could've patched the tube but decided to simply swap it and patch it later.
It took a while because it's my first time but I wasn't in a hurry.
There was a really nice bench nearby to work on and a small #creak to wash my hands in afterwards.
plane crash, american cultural imperialism
watching a video about an airplane crash titled "when the metric system kills" and the whole incident was actually caused by american cultural imperialism and the imperial system 
What's a good resource for folks who just discovered they're getting fëcked over by Big Font MegaCorp™ and want an alternative that's not one of the big free font providers?
Alternatives to the obvious services seem to be very well hidden from "regular webdev folk".
昨夜ビラノア飲むの忘れてて死ぬかと思った、イレギュラーだけど朝飲んだ
Oops
was trying to touch-up the glaze that crawled, and re-fire, but I slipped.
🇧🇪 #Belgium picks of the day:
➡️ 
@namipNAM-IP Computer Museum - Computing history museum in Namur (in French)
➡️ 
@UniversitedeLiegeUniversité de Liège - The University of Liège (in English & French)
➡️ 
@ikobIKOB - Museum - Contemporary art museum in Eupen
➡️ 
@Kunstenpunt - Flanders Arts Institute, supporting, promoting & researching art (in Dutch)
➡️ 
@ORB_KSBRoyal Observatory of Belgium - Royal Observatory of Belgium (in English, Dutch, French)
➡️ 
@Scivil - Centre for citizen science in Flanders
➡️ 
@worldofjoshWorldofJosh.be - Belgian urban exploration (in French & English)
🧵 1/4
via Sahel Sounds (on bandcamp at https://sahelsounds.bandcamp.com/ ):
Friends - we’re happy to announce that Etran de L’Aïr made it safely to the USA and will be kicking off their North America tour in Seattle tonight!
Check below for full dates and tickets. New merch available at the venues. Hope to see you in the crowd!
Also check out their brand new single “Agadez” if you haven’t already - etrandelair.bandcamp.com/track/agadez
Tour info behind CW in reply…
@
Atemu
Sara Joy 
