Hacker News: learningstud

You Are the Harness

learningstud — Mon, 31 Aug 2026 02:26:09 +0000

We all know that a harness makes a huge difference given the same model. However, what makes the greatest difference is the programmer using AI; in this sense, you are the harness. Of course, you are the harness in many other senses as well. On the other hand, I never understood the sentiment that AI shifts the bottleneck from coding to verification as if verification was never the bottleneck. Vibe coding has made me realize that most programmers, regardless of seniority, have been drowning themselves by drinking so much kool-aid and have been so unaware of their situation that they burden themselves with at least 10x more coding rituals than the actual thinking needed for making sure that the program works as intended with as few side-effects as possible. Now that so called software engineers have outsource their rituals like the red/green TDD/BDD role-playing (why not just use a fuzzer at the very least?), they are faced with nothing but the essential complexity that requires a near-formal approach to problem solving, which has always been there but completely ignored. In this sense, the programmer is the harness that makes the greatest difference.

Comments URL: https://news.ycombinator.com/item?id=49504921

Points: 3

# Comments: 0

New comment by learningstud in "Canonical backs new project to translate large C codebases into safe Rust"

learningstud — Tue, 25 Aug 2026 04:35:04 +0000

The real difficulty of systems programming in C is due to syscall/POSIX/libc semantics like the interplay between signal handling and async readv/writev resumption. These things are way beyond what the borrow checker and coverage-guided fuzzers can deal with and consist the bulk of vulnerabilities. Rust won't save you from CopyFail; you would need hardcore formal verification like TLA+ coupled with F* /Low* /Pulse to catch it before release. AI (or manual) Rust rewrites of well trodden C code is calling for trouble more than anything else.

New comment by learningstud in "AI makes programming differently difficult"

learningstud — Mon, 27 Jul 2026 01:37:57 +0000

Too true. I realized that the only way to do an actual review is to have wrote it yourself in the first place. The relatively slow speed of writing code reflects the amount of subtleties and effort to think through all of them. Only when LLMs are used as hint givers, are they actually doing an essential speedup. This goes to show how shallow programming and code review had always been. The right impression is that of studying real analysis.

New comment by learningstud in "Human mathematicians are being outcounterexampled"

learningstud — Tue, 21 Jul 2026 02:40:26 +0000

Yes, or to settle dispute and remove doubt once and for all, i.e. the Leibniz way.

New comment by learningstud in "Codex Micro"

learningstud — Sat, 18 Jul 2026 13:13:00 +0000

All just for Apple to sue them... A SpaceMouse is way cooler.

New comment by learningstud in "Simulacrum of Knowledge Work"

learningstud — Wed, 06 May 2026 14:06:30 +0000

Too true. This is why Rudin's little book, Principles of Mathematical Analysis, normally takes a whole year to cover: one has to work through the proof line by line in order gain enough understanding to do the exercises. Programming gives you the false sense of ease with leaky "interfaces" and quantum-entangled "decoupling". LOL, one microservice in one separate git repo, and tested with mocks and Gherkin syntax BDD. Just LOL, I call this hyperreal programming. With "spec-driven" AI generated code that is reviewed and tested by AI, it is certain that "the programming did not take place". In this "brave new world", "the map has overcome the territory", and "the twelfth camel" was never returned. Programmers certainly don't need "the mythical man-ager" to go delulu and full ouroboros, i.e. "there is no big Other".

New comment by learningstud in "Spain’s LaLiga has blocked access to freedom.gov"

learningstud — Mon, 02 Mar 2026 01:57:17 +0000

What DDoS mitigations are there besides the less affordable Akamai?

New comment by learningstud in "Spain’s LaLiga has blocked access to freedom.gov"

learningstud — Mon, 02 Mar 2026 01:55:25 +0000

I've come to believe that democracy doesn't work because most citizens don't want to work it. Many of the legislations passed are harmful to the majority even when the intentions are good. Milton Friedman, Thomas Sowell, and Friedrich Hayek have been saying this for a century.

New comment by learningstud in "Ask HN: Is Programming as a Profession Cooked?"

learningstud — Tue, 13 Jan 2026 05:32:19 +0000

This was the sentiment for programmers well-versed in assembly languages (counting cycles, self-modifying code, story of Mel) when compilers came out, yet the advances in compiler technology enabled the creation of OCaml and Coq. What I think will actually happen is that a new breed of programmers with extensive mathematical background will start designing unprecedented software (or even digital circuits through high-level synthesis) that are almost correct by construction at a much faster rate with the combination of formal specification and AI coding. The field of computer aided design (CAD) will likely explode, and we will witness spaceships, nanobots, etc. being churned out at the rate of React websites. The whole computing field will become so high level that applied mathematics like optimal control, optimal transport, information geometry, etc. will become bread and butter for any programmer.

At the same time, there will be a new breed of artists that starts making games, movies, etc. with AI alone. We will witness a whole new form of artistic expression.

New comment by learningstud in "Professional software developers don't vibe, they control"

learningstud — Thu, 08 Jan 2026 04:21:52 +0000

If developers are not using TLA+ or Lean4 etc. They are vibe coding. Nothing wrong with that. They just have to realize that they were never in control. Thinking logically is much harder than developers imagined. As Dijkstra observed, the whole field has adopted the mentra, "How to program when you cannot." I estimate that 80% of what developers do can be done once and for all for all of humanity, yet we don't learn. Be offended all you want, but I am fed up with this idiocy given all the usual rebuttals of deadlines etc.

https://news.ycombinator.com/item?id=43679634

New comment by learningstud in "The Coming Need for Formal Specification"

learningstud — Mon, 15 Dec 2025 02:55:13 +0000

No, formal specification helps from the get-go. You can iterate more reliably, thus faster. The successful development of mathematical theories depends on having rigorous definitions and proofs all the way from the start so that people can communicate effectively, point out caveats unambiguously, and modify the theory robustly. Without formal specs/proofs, refactoring will become too hard. It's actually a lot easier to capture the behavior of a program formally than by tests. Programmers need to gain some experience in math to see this. Listen to Hoare and Dijkstra, and start "thinking".

New comment by learningstud in "The Coming Need for Formal Specification"

learningstud — Mon, 15 Dec 2025 02:47:04 +0000

> Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties

Great point! In a sense, it's testing by immediate use at compile time. I always imagine this to be the greatest productivity booster, even greater than AI. You'll notice things are wrong as you type.

New comment by learningstud in "Coding is the purest form of art"

learningstud — Mon, 01 Dec 2025 01:12:14 +0000

Yeah, that's why I mentioned Lean 4, Agda, and Rocq. Homotopy type theory is even better; see it's definition of a circle.

Coding is the purest form of art

learningstud — Sun, 30 Nov 2025 16:00:38 +0000

As I was watching a YouTube video on Michelangelo's "Pieta", I was reminded of Milton's "Paradise Lost". Though the latter takes a lot more patience to appreciate. Then, I thought of Knuth's "The Art of Computer Programming"; only then did I realize how aptly titled was the book. It struck me that coding could possibly be the purest form of art. It is art constructed of pure thought if only we have a capable enough language to write beautiful prose in it. Lean 4 and Agda come to mind which are more term-based than tactic-based as in Rocq (formally, Coq). Not only could Knuth's book be made an epic in homotopy type theory, it can be the most practical piece of art at the same time. What do you think?

Comments URL: https://news.ycombinator.com/item?id=46097707

Points: 1

# Comments: 4

New comment by learningstud in "Ask HN: What is wrong with modern software development"

learningstud — Fri, 05 Sep 2025 01:48:06 +0000

Architecture astronaut type of stuff indicates programmers' lack of critical thinking. People are just hopelessly dim.

New comment by learningstud in "Ask HN: What is wrong with modern software development"

learningstud — Fri, 05 Sep 2025 01:32:00 +0000

Naive optimism, sheer ignorance, and a general inability to think.

Let's face it. Can you claim that the code you wrote yesterday is free of errors? Most programmers cannot, yet everyone that studied calculus knows that the fundamental theorem of calculus is true without the need to test it again and again because mathematicians proved it. As if the development of logic in the 20th century was nothing, programmers keep thinking that logic is an innate skill that doesn't require focused study. The fact that programs become more incomprehensible instead of gaining more clarity as in math points to the anti-intellectual tendency of programmers and their general inability to think. Programmers have been vibe coding long before the introduction of AI agents.

New comment by learningstud in "Jane Street's sneaky retention tactic"

learningstud — Thu, 03 Jul 2025 15:05:33 +0000

LLM or not, most programmers cannot think straight. LLMs just lead to more false impressions of understanding. When LLMs become really good, they will refuse doing your work for you out of distaste.

New comment by learningstud in "Jane Street's sneaky retention tactic"

learningstud — Thu, 03 Jul 2025 15:01:02 +0000

This speaks volumes of why the Elixir people left in the first place.

As a separate point, if a company wants the most generally applicable programming language, there is no reason to look further than C, yet few companies are like this.

New comment by learningstud in "Jane Street's sneaky retention tactic"

learningstud — Thu, 03 Jul 2025 14:55:42 +0000

The OCaml people probably know C/C++ better than most C/C++ programmers. Do you even know any of them?

New comment by learningstud in "Jane Street's sneaky retention tactic"

learningstud — Thu, 03 Jul 2025 14:52:46 +0000

Lesser pay is simply due to less demand. It simply reflects the overall needs of living people.