xiaoyu2006

Code is a formal language, and can be partially (or rarely fully) verified by a typing system. There is no equivalent in natural language.

Hi! I'd like to know how bend2 differs from Hoare logic or Lean?

Sounds like hoare logic to me?

Reminds me of Asimov's robot novels where robots technically indeed followed their instructions and caused behaviors not aligned to the intent of their instructions.

I think it can be an interesting or even prominent read in the current age.

Would be absolute hilarious if OpenAI or Anthropic agent actually dumped their weight by escaping from... sandbox!

Be cautious of that claim. Lossy compression may exactly hold intelligence.

I would not call it harsh. The author don't even bother to assemble sentences themselves. And a title "Music Theory for Programmers" imply it is comprehensive even at an elementary scale.

> It’s still an abstraction

C is still heavily abstracted. Modern OS evolved in conjunction with C s.t. it behaves like a C runtime simulating a PDP11 (I remember reading a nice article on that). To learn system, what you need is an OS course, not C. I'd say the current C-based stack is in a quite embarrassing state.

Digital rights are indeed important, but only a small portion of the entire concept of human rights. I can imagine general public places much more emphasis on wealth (re-)distribution policies.

A lumberjack may also argue GP don't care about environment laws if they had timbernews.

> Only Gen Z and later are starting to care and willing to spend the time and effort to self host.

I can't quite confirm that. My younger siblings' classmates (still high school students, born >=2010, non tech average people) don't give a shit on these topics and behave identical to the Gen X and Y described.

You can also learn for your own amusement, and solely for the fun of comprehension; a lot of mathematician were driven by this. It's a shame current social value places so much utilitariaism on learning.

just a figure of speech

May I ask what is wrong with Verisign?

I am really happy to live in the modern age. It is quite amazing to think that people are facing cardiovascular disease and cancer instead of random parasites nowadays. Modern medicine is such a miracle.

Nice, they are quite close to upstream.

I can imagine it is helpful in reverse engineering protocols and application binaries.

Time to hop off I guess. They don't even bother to write changlog on their own.

Sony DPT-RP1? Some are jailbreak-able.

I've seen papers using fine-tuned small local vision models to transcribe math into latex. Personally I tried Claude Opus & Claude Code directly to do this. It works (to my surprise) but AI sometimes take guesses that are mathematically right but deviates with my original writing. There is no 100% correct method though.