jderick

Bo Burnham

dev vs validation team

I think with guitar it is easy to enter flow state because it is easy to avoid playing the "wrong" notes. Probably similar to these other hobbies. Perhaps they just happen to have a tactile component, although it is nice to do something a little different from time to time. It seems computer games probably provide a similar form of satisfaction.

Can you put them all on one page and zoom in/out? Might be interesting to see some patterns in the sequence. Maybe allow filters for different factors or number ranges or different groupings.

Was this in SV?

Could this be used to train an LLM? It seems the hidden states could be used to learn how to store history.

Distributed systems are hard. I like the idea of "semantic locality." I think it can be achieved to some degree via abstraction. The code that runs across many machines does a lot of stuff but only a small fraction of that is actually involved in coordination. If you can abstract away those details you should end up with a much simpler protocol that can be modeled in a succinct way. Then you can verify your protocol much more easily. Formal methods have used tools such as spin (promela) or guarded commands (murphi) for modeling these kinds of systems. I'm sure you could do something similar with the lean theorem prover. The tricky part is mapping back and forth between your abstract system and the real one. Perhaps LLMs could help here.

I work on hardware and concurrency is a constant problem even at that low level. We use model checking tools which can help.

I wonder if this can generalize to mandelbulb?

Step one should be having an edtech ecosystem that doesn't allow students to use the web. There are just too many distractions online. I think noone has really invested the kind of capital required to do a good job with this. Most of the software my kids have to use for school is pretty bad.

It's a lot harder to make a single player game have depth and complexity than it is for a multi player game, since you don't have human opponents.

It doesn't make sense unless zooming out shows some higher level representation of the code.

It is interesting to see the type of analysis he does and the visualizations are impressive, but the conclusions don't really seem too surprising. To me, it seems the most efficient learning algorithm will not be simpler but rather much more complex, likely some kind of hybrid involving a multitude of approaches. An analogy here would be looking at modern microprocessors -- although they have evolved from some relatively simple machines, they involve many layers of optimizations for executing various types of programs.

I'd be curious to see an example of what you are talking about wrt his analysis here.

What is GPR?

Even great regular coffee isn't ubiquitous yet.

For me, reading fiction is all about beauty. I liken it to listening to good music. It isn't really to learn anything "substantive." It is to experience a feeling or be transported to another place. In fact, I like to listen to (typically instrumental) music while I read as a sort of "soundtrack." I would liken reading a good book to watching an epic movie. I guess you might occasionally gain some insight into the human condition, but it isn't primarily an informational medium.

For me, Joyce is the pinnacle of the English language. I can't say I understand too much of what is happening but noone writes more beautifully. I just love the sound of his words and the images he conjures.

Maybe they can create one without all the traffic.

Apple is pretty tight lipped about revealing the details of our work. Formal is a bit of a niche area, but you can find some info online.

Here is a course taught at UT with some slides from guest lecturers from industry that looks like a decent overview:

https://www.cerc.utexas.edu/~jaa/verification/

Also, the main conference in the area is FMCAD, you can find a lot of related work there. More recently the conference has moved more towards software, but if you look at some of the older proceedings you can find a lot of hardware related stuff.

https://www.fmcad.org/

There is decent amount of overlap between formal for hardware and software, so if you study one you will likely have enough background to get started in the other.

We use formal at Apple to verify hardware. We are always looking for good people in this area.

Maybe instead of a summary we should ask what the most interesting parts of the article are?

I wonder if the gap has narrowed over time.

Or even better, remote work.

tldr:

"So you're saying the best way of figuring out what's inside someone else's mind is to ask them?"

"That's right."

Isn't EVE like this?

Yes, vegetable oil is typically soybean oil.

I don't think kids today would be as interested in an Apple II today as we were as kids. The games and things they can do on a computer now are far beyond that and it just doesn't hold their interest.

My kids have done some basic programming in scratch, which I think is a good place to start. I also once set up godot with a simple open source game that they could edit (change sprites and adjust parameters like speed/size etc). They enjoyed that. I think once they want to start doing something more advanced, something like roblox or minecraft modding might be a good place to get their interest. Shadertoy/GLSL might be another fun thing to start with at more a high school level.

You could also punish people who vote for unpopular content. Similar to how captchas work, if you vote in the minority, you could be assumed to be a 'bot'. This would also require some kind of ML to account for your interests, so you would be compared against others with similar interests.

The movie "Brazil" remade in modern day Sweden.