Viewing profile — agentultra

Tania Aelbi wrote a good one of her trip. I’m working towards a solo circumnavigation myself. Love reading about the stories of others.

Or anyone else! This isn’t for the protection of kids. It’s for the protection of profits by surveillance capitalism.

I think the controversial part is that an engineer cannot talk to or understand customers.

A test doesn’t prove much. Highly experienced programmers seem to have a hard time understanding this. Why do we have tens of thousands of test cases and we still find new errors c…

Apparently it is. Modern companies seem to prefer dysfunction over anything else. I have been trying to understand why for my whole career.

I don’t disagree. I’ve worked on teams that definitely valued the non-coding skills more and it showed in their inability to deliver on certain requirements… mainly performance and…

The author might be missing the intent of the observation. Maybe they’re misinterpreting it. What I, and many people who’ve said, “code was never the hard part,” aren’t referring t…

I think people are one factor. Source does, when done well, communicate intent and implementation precisely to other people . If the language has enough semantic information it can…

The market logic isn’t going to be defensible. The market is highly irrational and prone to be influenced by those with the most capital, not the, “invisible hand.” Cars are freaki…

> I do not miss the wall, and I will not pretend to. The wall is the point, if you want to truly know the truth of something. I still believe there is no royal road. Taste isn’t th…

Simulating Elevators in TLA+ is a fun exercise. https://github.com/tlaplus/Examples/blob/master/specificatio... Another interesting, and underrated one: hotel keys.

This brings me back. I got to work at a movie store for a while. Great times. Almost like Empire Records.

I believe there’s a small minority of LLM users who will show up to any comment thread and scream bloody murder if you post any kind of policy limiting LLM use. They seem to feel l…

That would be an example of, “overfitting.” It is something the AI labs are concerned about. They tweak parameters to try and avoid it. It’s a hard balancing act to do. Give in too…

Okay so in the sense of Lean’s kernel, we can trust it as long as we understand it. Verifying it cannot be automated therefore, according to the criterion, it must be small so that…

Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how …

What I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec? Is there an implicit trust we must put in that kernel?

> A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-w…

Building a MUD engine is quite an endeavour in itself. Let alone the game! A good way to test your skills in networking, parsing, databases, and data structures. I’ve been chipping…

It’s a big tent and anyone is welcome in. I learned to code on my own thanks to the efforts of people to write manuals, articles, text files on BBSs and NNTP. That’s just one way. …

Their adoption results are going to be biased by the fact that Google has a vested interest in accelerating adoption and have been sticking their AI products in front of everything…

You should check out Borges’, The Library of Babel . Basically if you have an infinite string of characters in some language then you have every possible book, tweet, script, scrib…

This seems to be grasping for analogies to make sense of the work this person was doing. A compiler does a lot more than source code translation. There are specifications that tell…

That will depend on your life goals.

There are cabinet makers who still make pieces by hand with hand tools. They charge whatever they want and do well. Not everything is Ikea.