HN user

rck

1,374 karma

I'm into robotics and machine learning.

Posts57
Comments69
View on HN
tannerduve.github.io 1y ago

Verified dynamic programming with Σ-types in Lean

rck
86pts43
lemmata.substack.com 1y ago

It's Not What You Think: LLMs Like Obvious Answers

rck
3pts0
web.stanford.edu 1y ago

Functional Programming and Theorem Proving in Lean 4

rck
6pts0
github.com 1y ago

Show HN: Easily generate text and compute probabilities for any Hugging Face LLM

rck
2pts0
richardkelley.io 2y ago

Building a Local LLM Agent with Speech Recognition and TTS Support

rck
1pts0
github.com 2y ago

Show HN: Dendron – A Library for Building LLM Agents Using Behavior Trees

rck
2pts0
eugeneyan.com 2y ago

Language Modeling Reading List (To Start Your Paper Club)

rck
1pts0
aizi.substack.com 3y ago

How does GPT-3 spend its 175B parameters?

rck
3pts0
faultlore.com 3y ago

Text Rendering Hates You

rck
3pts0
buttondown.email 3y ago

Formalizing Stability and Resilience Properties via TLA+

rck
3pts0
zed.dev 3y ago

Leveraging Rust and the GPU to render user interfaces at 120 FPS

rck
259pts203
30fps.net 3y ago

Full screen triangle optimization

rck
115pts44
cs.paperswithcode.com 3y ago

Evaluating the Cost of Atomic Operations on Modern Architectures

rck
2pts0
rauljordan.com 3y ago

Rust concepts I wish I learned earlier

rck
379pts170
coredumped.dev 3y ago

Design of Emacs in Rust

rck
3pts0
rodneybrooks.com 3y ago

Predictions Scorecard, 2023 January 01

rck
6pts1
www.lpalmieri.com 3y ago

A taste of pavex, an upcoming Rust web framework

rck
2pts0
wtgowers.github.io 3y ago

Human-Oriented Automatic Theorem Proving

rck
42pts17
blog.janestreet.com 3y ago

Accelerating ZK-SNARKs – MSM and NTT Algorithms on FPGAs with Hardcaml

rck
27pts0
scrtwpns.com 4y ago

Practical Pigment Mixing for Digital Painting

rck
60pts13
freedombox.org 5y ago

FreedomBox: Run your digital services from your home

rck
265pts75
banditalgs.com 7y ago

Bandit Algorithms Book

rck
4pts0
www.wired.com 7y ago

RIP Anki: Yet Another Home Robotics Company Powers Down

rck
3pts0
www.extremefinitism.com 8y ago

Extreme Finitism – Banish Infinity for Good

rck
3pts0
www.washingtonpost.com 8y ago

‘I am thoroughly ashamed’: British lord resigns after arriving late to work

rck
2pts0
www.theverge.com 8y ago

Boston Dynamics’ latest robot dog is slightly less terrifying

rck
2pts0
mobile.nytimes.com 8y ago

Tech Giants Are Paying Huge Salaries for Scarce A.I. Talent

rck
5pts0
news.fastcompany.com 9y ago

HoloLens is still for developers, developers, developers

rck
2pts0
www.wired.com 9y ago

Mapped: The Top 263 Companies Racing Toward Autonomous Cars

rck
2pts0
www.wired.com 9y ago

Don’t Look Now, but Even Buses Are Going Autonomous

rck
1pts0

Yeah, for professional robotics you just accept that this is the world we live in. But for learning and hobbyist stuff, it's better to play with simple hardware and build the things that ROS is ultimately abstracting over before you try to pick up ROS.

I've seen people get sucked into ROS + simulation who end up never touching real robots. Which is fine if that's what you want to play with, but it's debatable if "ROS + sim" alone is even "robotics."

The thing that most people don't appreciate is that ROS was co-designed with the PR2, which had a very idiosyncratic architecture: two separate computers in the base, ethercat for comms, not at all modular, and very high end parts (for 2010ish). Most of the weirdness of ROS looks less weird in light of the design of the PR2, and most of the evolution of ROS was to get away from the PR2 model for more general platforms.

If you were in robotics prior to 2010, you probably would have used something called Player/Stage (by some of the same people who developed ROS). Believe it or not, another big motivation for ROS was solving the (many) problems that popped up as people tried to get Player/Stage running with robots like the Pioneer 3-DX.

Get an arduino kit and learn a little electronics. The kit likely comes with a brushed motor and a servo. Learn how motors works and how to write code to make motors spin. Then get a stepper motor and an arduino-compatible motor shield or CNC shield and spend some time getting multiple motors to move. Once you understand those basics, you can hook motors together in a rigid frame and you have a robot (2 motors with wheels is mobile, 3 or 4 motors with links is an arm). The kit will also come with some simple sensors which you can use to do things like measure light and distance, which you can use to start playing with feedback control (look up Braitenberg vehicles for a project idea).

Seconding all the people who said avoid ROS - it's not worth the effort for hobby-level stuff. It's barely worth the effort for "professional" robotics.

Also don't worry about physics too much - build your physical intuition by playing with working systems of increasing complexity.

What Is Stoicism? 6 months ago

The Stoics are explicitly mentioned in Acts of the Apostles, but I think a better way to think about it is that the framework of "Virtue" as "Conforming to your Nature" is a very useful one for understanding the gospels, as was developed extensively starting in the mid 1200s.

What Is Stoicism? 6 months ago

It's interesting that the main thinkers listed are all Roman. They're definitely the best known, but Stoicism was a Greek philosophy first and foremost, and Cleanthes, Chrysippus, etc. were more significant than any of the Romans.

Stoicism had a lot going for it, but it was also full of a lot of crazy nonsense - there's a reason you've never met a Stoic who was fully on board with Stoic natural philosophy or "physics." The logic eventually made a comeback (via Frege, possibly due to plagiarism!), and the virtue ethics got absorbed into Christian moral philosophy by about the 13th century (by way of neo-platonists who influenced Dominican philosopher theologians like Aquinas). It's not surprising that it ran out of steam.

Yeah it looks like about 1500 grants:

https://www.urban.org/urban-wire/nsf-has-canceled-more-1500-...

But if the concern is about the provision allowing NSF to claw back funds that have been spent by the organization then the question remains: has that happened? Right now if you search for terms related to NSF clawbacks, most of the top results refer to the PSF's statement or forum discussions about it (like this one). I can't find any instances of a federal clawback related to DEI. If that had happened I would assume that the response from the awardee would have been noisy.

I can imagine that a very risk averse lawyer would have pointed out the costs and uncertainties of litigation in cases like this. But if I were in their shoes and I really cared about the money, I would have pressed that lawyer to show examples where the clawback clause had been invoked since Jan 20. I'm not sure it's happened, which seems relevant to estimating the actual risk.

Interestingly, they may get more in donations than they would have from this grant, so maybe that needs to be including in the risk estimate as well...

Not a lawyer, but the NSF clause covering clawbacks is pretty specific:

NSF reserves the right to terminate financial assistance awards and recover all funds if recipients, during the term of this award, operate any program in violation of Federal antidiscriminatory laws or engage in a prohibited boycott.

A "prohibited boycott" is apparently a legal term aimed specifically at boycotting Israel/Israeli companies, so unless PSF intended to violate federal law or do an Israel boycott, they probably weren't at risk. They mention they talked to other nonprofits, but don't mention talking to their lawyers. I would hope they did consult counsel, because it would be a shame to turn down that much money solely on the basis of word of mouth from non-attorneys.

I'm not sure what motivated Parmenides because he was more of a poet than anything - it just happened that his poetry was what we would now recognize as incredibly philosophical. He didn't really argue, he just wrote down what the "goddess" told him. But I think the basic problem is that everyone back then agreed that you can't get "something from nothing," and it sure seems like change requires being to come from non-being. The statue is there now, but before it was cast there wasn't a statue, just a chunk of bronze. If being can't come from non-being, how do you account for the "coming-to-be" of the statue? The Eliatic position as I understand it is that the change is just an illusion. Plato and Aristotle both react against this position and argue that it's silly (I'm very inclined to agree). They then give alternative accounts of what change really is.

I'm not sure about Plato, but the Aristotelian analysis is something like this: every thing that exists has the potential to exist in certain ways and not others, and it's said that the thing is "in potency" to exist in those potential ways. When something could exist in a certain way but right now doesn't, that's called a "privation." And the ways that the thing currently does exist are the "form" of the thing. So a substance changes when it goes from being in potency to being actual, and it does that by losing a privation. Aquinas follows Aristotle in giving the example: "For example, when a statue is made from bronze, the bronze which is in potency to the form of the statue is the matter; the shapeless or undisposed something is the privation; and the shape because of which it is called a statue is the form." Incidentally, Aquinas's short On the Principles of Nature (https://aquinas.cc/la/en/~DePrinNat) is a good overview of this theory, which is spread all over Aristotle (in the Categories, the Physics, and the Metaphysics).

As far as οὐσία is concerned, I think this is the complete Greek for Parmenides's poem: http://philoctetes.free.fr/parmenidesunicode.htm. In the places where that translation uses "being" you get slightly different words like γενέσθαι (to come into a new state of being) or εἶναι (just the infinitive "to be"). And looking at the definition of οὐσία (https://lsj.gr/wiki/%CE%BF%E1%BD%90%CF%83%CE%AF%CE%B1) it looks like most of the uses of that term specifically come well after Parmenides.

This is fun. But the bit at the beginning about philosophy is not correct. Parmenides did not believe in what we would call essences, but really did believe that nothing ever changes (along with his fellow Eliatic philosopher Zeno, of paradox fame). The idea that change is an illusion is pretty silly, and so Plato and especially Aristotle worked out what's wrong with that and proposed the idea of _forms_ in part to account for the nature of change. Aristotle extended Plato's idea and grounded it in material reality which we observe via the senses, and that's where the concept of essence really comes from - "essence" comes from the Latin "essentia" which was coined to deal with the tricky Greek οὐσία (ousia - "being") that Aristotle uses in his discussions of change.

The Nevada Museum of Art had an exhibit last year about Picasso's ceramics, and I was amazed at how ... meh it all was. Apparently the market agrees with me, because you (yes you!) can buy a Picasso plate for just a few thousand dollars.

Pope Pius XI wrote about _subsidiarity_ as a guiding social principle:

"Just as it is gravely wrong to take from individuals what they can accomplish by their own initiative and industry and give it to the community, so also it is an injustice and at the same time a grave evil and disturbance of right order to assign to a greater and higher association what lesser and subordinate organizations can do. For every social activity ought of its very nature to furnish help to the members of the body social, and never destroy and absorb them."

Tao is observing the consequences of a society that increasingly has abandoned subsidiarity as an operating principle. (I had hoped that crypto might be able to bring subsidiarity back, but so far the opposite has happened in practice.)

This feels like the kind of popsci that's written for people who already agree with the author - there's nothing resembling an argument, or even a definition of "computation." There are nods to Church-Turing, but the leap from "every effectively calculable function is computable" to "life is a computation" is larger than anything you could fit in a book.

For the sake of comparison, you can train a 124M model on a 3090 (see nanoGPT). In that case, each batch ends up having about 500,000 tokens and takes maybe around 10ish seconds to run forward and backward. Then the 6 trillion tokens that this model was trained on would take about 4 years, approximately. Or just "too long" for a shorter answer.

GPT-5 12 months ago

You are underestimating the hype around self-driving. A quick search gives this from 2018:

https://stanfordmag.org/contents/in-two-years-there-could-be...

The open (about the bet) is actually pretty reasonable, but some of the predictions listed include: passenger vehicles on American roads will drop from 247 million in 2020 to 44 million in 2030. People really did believe that self-driving was "basically solved" and "about to be ubiquitous." The predictions were specific and falsifiable and in retrospect absurd.

Do you know of any short examples of this? Yesterday I was trying to prove some "easy" theorems that involved machine number representations, and I couldn't find anything in Lean.

They're claiming some revolutionary "synthetic muscle," but is there video of one of these things walking? If it's just pneumatics then this is a repeat of the early androids out of Japan, which looked cool but never got up and moved - they were basically just impressive animatronic dolls. My guess is that this ends up being something similar.

DeepSeek-R1 2 years ago

It's interesting that, at least through ollama, it appears impossible to get DeepSeek-R1 to give concise answers to questions that don't require any reasoning.

Before you read this, it's worth your time to check out Haraway's Wikipedia page. The criticism section sums things up nicely:

Haraway's work has been criticized for being "methodologically vague" and using noticeably opaque language that is "sometimes concealing in an apparently deliberate way". Several reviewers have argued that her understanding of the scientific method is questionable, and that her explorations of epistemology at times leave her texts virtually meaning-free.

This manifesto is exactly the kind of nonsense that led Alan Sokal to send his fake paper to Social Text. Essays like this should come with a Surgeon General's warning: this writing may be amusing, but if you take it seriously it will rot your brain.

Tangential, but: the notes that this post refers to are probably not the best way to learn how transformers work. If you want mathematical precision, those notes are based on this paper from DeepMind:

https://arxiv.org/abs/2207.09238

The paper provides mathematically precise definitions of all the parts of a transformers, though it's showing its age (ha!) in that it doesn't include some formalizations that are common in, for example, Llama.