Verdex

Fearmonger? Me? Well I never.

Also

> if you've worked with other proof oriented languages.

That's doing a lot of heavy lifting.

To borrow your video game analogy. F* is the dwarf fortress of programming languages. Screenshots are only going to confuse anyone who isn't ready to take a significant mental journey.

It has to be done by next week.

Here it is. It is done.

Great, now we put it on a shelf and ignore it for 6 months.

From my perspective, every time.

Edit: the last time this happened to me, they later revealed that it was going to be shelved for a year.

Today we see someone being arrested because they used a software feature. Next year we'll see someone being arrested because they played a cutesy trick and got the LEO to enter in the self destruct code.

The engineers and techies involved have so far shown themselves to have poor intuition for understanding how the law is going to react. I think it behooves anyone still listening to their advice to also check in with someone who has a good intuition for how the law will react to this new idea.

This is an interesting idea, but was that GrapheneOS person a lawyer giving legal advice?

At least for me, the technical chops to be able to program a computer was always just table stakes for software engineering.

The majority of my job more or less reduces to mitigating the consequences of having all the stakeholders dreams come true. Most normal people consider rules as run by people. They expect them to ignore rules that don't make sense, apply rule of thumb, get the gist, and do what it takes to achieve success.

When you take these sorts of rules and try to put them into silicon, the end result is often an undesirable result despite all the rules being successful implemented.

The law are these sorts of rules. They're designed to be "executed" by people using judgement. Part of the reason why the law works is specifically because we don't have a bunch of computers watching everyone all the time. Secure in your person and papers is literally right there in the constitution. Like they didn't know about computer surveillance when they added that amendment but they knew that without privacy the law doesn't work as intended.

Which seems a bit off to me. Can they even ipo right now due to the apple business?

Although I don't think you're wrong. The number of "organic" social media posts I've seen in the past few weeks of the form: 'Wow, Anthropic users are ugly losers...nothing like those handsome openai tiger blood winner sages' is simply too high in my mind for anything other than an ipo prelude.

[Also are altman and musk really fighting on x? Like, that's got to be a sign of some sort of internal stressors right?]

This isn't a great comparison.

Im not that familiar with elixir, but erlang is hands down the best dynamic language to build systems in. It feels like they made only right decisions. I can only assume that elixir has made improvements on that.

Meanwhile java and kotlin have the least useful types I've encountered in my career. Scala has some pretty powerful stuff, but it's like the c++ of powerful types. The ergonomics aren't great. Finally, typescript has a lot of impressive typing constructs but it really falls down on the runtime side (because javascript).

The real comparison to make would be erlang/elixir vs rust or ocaml.

My first web search (data blades) turned up harbor freight woodworking tools.

Then I made a second web search: data blades database.

That turned up some ibm database software module technology which I assume is what's being discussed.

I created a personal philosophy of code awfulness because back in 2012 I worked in a code base that was so bad it completely baffled all my attempts to categorize it.

This and thus is why code is bad. Oh wait a second. They're doing something terrible that's completely orthogonal to the sum total of awfulness encounter so far.

The best (worst?) one was a demonstration mode that the product had. Functions would call functions, one after the other until like 50 calls deep you would wind up where you started. Why didn't the stack blow up? Because they would at seemingly random launch a new thread and abandon the existing stack. This was the main loop.

Simply describing the mess was enough to convince the client to let us rewrite the feature wholesale.

Anyway the point is the same as yours. Slop code is a thing long before our current scenario.

Okay ..

However given the history of mathematics that's not really out of order. There's a lot of mysticism intertwined with early mathematics and it's only relatively recently that mathematics has taken the beads out of her hair, put on a business suit, and gotten to work.

I mean even Galileo's, the patron saint of skepticism, job was observing the stars so that he could write horoscopes.

And we see the attitude repeated even today. I work in a technical field and whenever I mention that I think type theory is kind of cool the response more often then not is for them to give me the ol' "Thank goodness for people like you, I'm just not a math person."

The way I look at it, the absurd complexity that rule systems can get into is a check and punishment for the arrogant and the tyrannical. 'Look I designed these rules myself just follow them and everything will be fine.' Ah but what about this edge case. 'Hm, I guess we can add a few more rules.' Bam, next thing you know it's a Byzantine bureaucratic nightmare any your empire refuses to grow anymore.

Meanwhile, if you put honorable people in charge and trust them to do the right thing, they can figure things out ad hoc.

Unfortunately, mathematics suffers as a bystander. But the good news is that the muggles will always want to keep the eggheads around because they would rather die than think about the negative consequences of having their dreams come true exactly like they wanted.

Cheaper is skipping a step.

Code duplication and 'wrong' abstractions both count themselves amongst the other foibles of programming. But they don't directly produce a cost which can be cheap or expensive.

They produce some other high dimensional intermediate value which can then produce highly variable cost dependent on the domain, goals, and scenario.

As ever, it depends.

The depends is quantifiable, but it doesn't fit in a blog post. Think more along the lines of war and peace.

No it's not.

Also read the link. This is apache 2 licensed. Even in whatever imaginary world where there is such a social contract, there is thankfully a legal contract that includes disclaimer of warranty.

Chimp isn't, but at the end of freeze frame Sunday addresses one who she thinks is. [Not sure if that was the original intent in this thread, though]

> AI is completely different.

Okay?

> existential angst

I don't know, maybe there's just too many juniors on social media posing as senors spreading existential angst? I mean if GC was introduced in a time where there was an engagement AI spreading dread far and wide then I suspect we could have had the same thing.

I certainly wish people would be less sad, but I'm not sure that means that things are meaningfully different on a technical level.

It is?

Covid overhiring, no more 0% interest rates, that one accounting change, and companies needing a "growth" sounding way to announce layoffs. Maybe that's bringing actual layoffs in the name of AI?

This here.

Overall society feels more turbulent, but this is otherwise all the same song and dance all over again.

The 90s and 00s had this wave of "object oriented programming changes everything". Hey we're doing this thing that's been done successfully 100s of times before, but now it's OO. Writing some code in involving an airplane? Just purchase this omni-airplane object that does everything for airplanes (an actual thing I was told in college).

That's weird OO isn't the be all end all? Code gen, get this Ruby on rails running. Look at me building this website in two seconds. Code gen everywhere.

Huh, that's going to a funny place... TDD. If you aren't TDDing then you're such a bad engineer that you should be locked in prison (real conversation I observed). Oh wait, not TDD, BDD. That fixes it.

Lean, no Agile, no agile like with a small a ... but it was first, no scrum, no xml wait that was last decade, json, and finally SAFe.

Hey, have you seen this chat bot thingy?

Every iteration brings good stuff if you're paying attention. But it also brings a lot of hype and anxiety. Experiment and learn.

The one thing that's remained constant for me is that nearly everyone would rather die than to think carefully about the consequences of their dreams coming true. And as long as that remains true they'll continue to pay for someone else to ride the hype dragon on their behalf.

Hey, would you mind elaborating a bit on this:

> assuming you have a clear idea of what you want to do and how

I mean, if I have a sufficiently clear idea of what and how, then surely just coding it manually would work significantly better. Unless maybe I am a painfully slow typer.

Without some level of "actually I'm not sure exactly" permitted, then I'm not really sure what LLMs bring to the table.

Yeah, I think so. If someone lets you cheat off of their test, that's authorized but still plagiarism.

IIRC they do some stuff with f co algebras. Which if I understand it is effectively doing things like "hey here's a generator that produces an infinite number of the number 1, but the only way to evaluate it is via a take with a finite number".

I know with idris there is also a progress evaluator for otherwise general recursion that proves that your input is always "getting smaller". Not sure if charity has the same deal or not.

Regardless, it isn't turning complete, but the interesting part is how far you can get in a sub turing environment.

That's my take as well. I've had my unPRed branches grabbed up and blindly merged by an agent twice now. The guy doing it was shocked both times that his PR had my change sets in it.

Also one engineer is treating the code as assembly. I've asked some pointed questions about code in his PR and the response was "yeah, I don't know that's what the agent did".

Edit:

To everyone freaking out about the second guy. Yeah, I think being unable to answer questions about the code you're PRing is ill advised. But requirement gathering, codebase untangling, and acceptance testing are all nontrivial tasks that surround code gen. I'm a bit surprised that having random change sets slurped up into someone else's rubber stamped PR isnt the thing that people are put off by.

I have a friend who dealt with this in highschool. The English teacher just copied whatever their grade was from their first assignment onto all other assignments.

It got so bad that his Dad, who was an active English and Spanish teacher at another school, was convinced to write one of his papers for him. He got a D.

Heres the thing about clean code. Is it really good? Or is it just something that people get familiar with and actually familiarity is all that matters.

You can't really run the experiment because to do it you have to isolate a bunch of software engineers and carefully measure them as they go through parallel test careers. I mean I guess you could measure it but it's expensive and time consuming and likely to have massive experimental issues.

Although now you can sort of run the experiment with an LLM. Clean code vs unclean code. Let's redefine clean code to mean this other thing. Rerun everything from a blank state and then give it identical inputs. Evaluate on tokens used, time spent, propensity for unit tests to fail, and rework.

The history of science and technology is people coming up with simple but wrong untestable theories which topple over once someone invents a thingamajig that allows tests to be run.

Hey friend, check the user name of the person I'm responding to (and perhaps check out the people responsible for dtrace and larry ellison lawnmower comparisons). I might appear more coherent afterwards.

Whenever the lawnmower thing comes up, I try to also mention dtrace. As far as things to be remembered for, they make some strange bedfellows... although it's better than anything I've managed so I guess congrats.

While the LLM rust experiments I've been running make good use of ADTs, it seems to have trouble understanding lifetimes and when it should be rc/arc-ing.

Perhaps these issues have known solutions? But so far the LLM just clones everything.

So I'm not convinced just using rust for a tool built by an LLM is going to lead to the outcome that you're hoping for.

[Also just in general abstractions in rust feel needlessly complicated by needing to know the size of everything. I've gotten so much milage by just writing what I need without abstraction and then hoping you don't have to do it twice. For something (read: claude code et al) that is kind of new to everyone, I'm not sure that rust is the best target language even when you take the LLM generated nature of the beast out of the equation.]

It's also less frustrating to organize world wide ram production and logistics than to deal with a single mathematician.

Constantly sitting around trying to solve problems that nobody has made headway on for hundreds of years. Or inventing theorems around 15th century mysticism that won't be applicable for hundreds of years.

Now if you'll excuse me I need to multiply some numbers by 3 and divide them by 2 ... I'm so close guys.

Known in the business as 'pulling a jevons'

I suppose that you could have the phone listening in real time and generating profiles that are hidden and embarrassing but not illegal.

So when they ask for the real profile it shows in the next unlock a profile that makes it very clear you have a deeply embarrassing ASMR addiction.

It could cross reference your local laws to ensure to not spill the beans on something locally illegal.