madmax96

This is exactly what model-based systems engineering tools like SysML v2 are designed for. Model-based systems engineering aims to generate _all_ engineering artifacts from a formal model.

Imagine it -- security policies, infrastructure, etc. all codified in a formal model.

- Push-button generation of ISO-27001 documentation.

- Push-button generation of Terraform.

- Push-button generation of SpiceDB policies.

- ...

There is _a lot_ of missing technology, but this is critically important because it will help us ensure regulatory compliance at far greater speeds in fields like nuclear and automotive. And it enables automated reasoning over the models, to make sure you're actually doing what you set out to do.

Came here to say pretty much this. Hardware seems more valuable than a model.

I think AI could be commoditized. Look at DeepSeek stealing OpenAI's model. Look at the competitive performance between Claude, ChatGPT, Grok, and Gemini. Look at open weight models, like Llama.

Commoditized AI need used via a device. The post argues that other devices, like watches or smart glasses, could be better posed to use AI. But...your point stands. Given Apple's success with hardware, I wouldn't bet against them making competitive wearables.

Hardware is hard. It's expensive to get wrong. It seems like a hardware company would be better positioned to build hardware than an AI company. Especially when you can steal the AI company's model.

Supply chains, battery optimization, etc. are all hard-won battles. But AI companies have had their models stolen in months.

If OpenAI really believed models would remain differentiated then why venture into hardware at all?

Is bandwidth the limiting factor or is it ping?

Granted, it’s not restrictive if you only want to use Nix for general utilities and Unix libraries. But it’s extremely restricting if you want to use Nix to manage macOS apps. And I love Nix, so of course I want to do that :)

Thanks for posting the link to sponsor this work.

I love nix on macOS. But one word of caution: nix uses a very outdated, EOL’d, macOS SDK (https://github.com/NixOS/nixpkgs/issues/101229).

This post contains a number of statements that mislead the reader into believing that we are overreacting to memory safety bugs. For example:

> An oft-quoted number is that “70%” of programming language-caused CVEs (reported security vulnerabilities) in C and C++ code are due to language safety problems... That 70% is of the subset of security CVEs that can be addressed by programming language safety

I can’t figure out what the author means by “programming language-caused CVE”. No analysis defines a “programming language-caused CVE”. They just look at CVEs and look at CWEs. The author invented this term but did not define it.

I can’t figure out what the author means by “of the subset of security CVEs that can be addressed by programming language safety”. First, aren’t all CVEs security CVEs? Why qualify the statement? Second, the very post the author cites ([1]) states:

> If you have a very large (millions of lines of code) codebase, written in a memory-unsafe programming language (such as C or C++), you can expect at least 65% of your security vulnerabilities to be caused by memory unsafety.

The figure is unqualified. But the author adds multiple qualifications. Why?

[1] https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...

>For methods modifying internal state, I think you’ll have a hard time with the assertion that “purity is easier to reason about”.

Modeling the method that modifies internal state as a function from old state to new state is the simplest way to accomplish this goal. I.e., preconditions and postconditions.

>Prove it.

Proofs are good evidence that pure functions are easier to reason about. Many proof assistants (Coq, Lean, F*) use the Calculus of Inductive Constructions, a language that only has pure, total functions, as their theoretical foundation. The fact that state of the art tools to reason about programs use pure functions is a a pretty good hint that pure functions are a good tool to reason about behavior. At least, they're the best way we have so far.

This is because of referential transparency. If I see `f n` in a language with pure functions, I can simply lookup the definition of `f` and copy/paste it in the call site with all occurrences of `f`'s parameter replaced with `n`. I can simplify the function as far as possible. Not so in an imperative language. There could be global variables whose state matters. There could be aliasing that changes the behavior of `f`. To actually understand what the imperative version of `f` does, I have to trace the execution of `f`. In the worst case, __every time__ I use `f` I must repeat this work.

Dependently typed languages make it even better.

For example, in Lean4:

  def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠ 0) : Nat
    :=
    if denominator > numerator then
      0
    else 
      1 + myDiv (numerator - denominator) denominatorNotZero
  
  -- Example usage.
  example : myDiv 1 (denominator := 1) (by simp) = 1 := rfl
  example : myDiv 120 (denominator := 10) (by simp) = 12 := rfl

You have to submit a proof that the denominator is non-zero in order to use `myDiv`. No monad required ;).

It doesn’t matter if students know what to expect.

An oral exam isn’t the same as reading a written exam out loud. There are a set of learning outcomes defined in the syllabus. The examiner uses the learning outcomes to ask probing questions that start a conversation - emphasis on conversation. A conversation can’t be faked. A simple follow up question can reveal a student only has a shallow understanding of material. Or, the student could remember everything they’ve been told, but fail to make connections between learning outcomes. You can’t cram for an oral exam. You have to digest the course material and think about what things mean in context.

After all, students know what to expect on standardized tests. Some still do better than others :-).

Why does Ubuntu almost always perform better on the vec GPU benchmarks but not the scalar benchmarks? Is there a trade off here?

The whole situation is really confusing.

Some people already ``adjust'' their names for a Western audience, and others don't. So, given the <name 1> <name 2> of a Japanese person, I don't know if <name 1> is the family name or given name. Some people already make the adjustment so that Westerners get it right, some don't.

I don't care either way -- I'd just prefer things be consistent so that when I recognize a Japanese name I can call them by the proper name faster :).

Even dynamically typed languages like CL have type systems. However, CL implementations are under no obligation to statically check that a program is type-safe. Those checks are deferred until run time — hence the author’s complaints.

Airbnbs only make sense in rural areas. Hotels are more competitive in terms of price and location inside of cities. Cities have enough to do that I don’t want to be inside of my room that much during my trip, so space and TV simply don’t matter to me.

Nice article. I discovered this myself recently, but in a slightly different context: Taking the union of two sets represented as arrays. To my surprise, sorting the arrays and iteratively computing their union was faster than a hashset.

Others in this thread have mentioned that computing the hash takes time. This is true. Let n be the size of the array. When n in small, the (constant) overhead of computing the hash >> O(n * log n) sorting. Now, consider what happens as n becomes large: Virtually every access becomes a cache miss. The (constant) overhead of a cache miss is >> O(n * log n). At the time, I did the math, and determined that n would need to be some unreasonably gargantuan quantity (on the order of the number of stars in the visible universe) before log n is big enough to overtake the effects of cache misses.

>And before you mention the 3rd world needs crypto as a "usecase"

I'm an American. I got into crypto completely by accident. I needed to quickly send a large amount of cash to a family member out-of-state. I couldn't wire the money due to transfer limits on my family member's account. My banker told me it would take up to a week for a personal check to clear. My bank charges $10 for a cashier's check. FedEx told me it would be $65 to overnight the check.

Someone suggested I try Bitcoin. I purchased the amount in Bitcoin on Binance for no fees. I sent the Bitcoin to my family member for a transaction fee <$3. They received the amount within an hour. Within another hour, they had converted back to fiat.

Bitcoin solved a problem for me, as an American. I'd be glad to learn of a cheaper, easier alternative.

>It seems plausible to me that the price elasticity of demand[1] for eggs is small

Agreed.

>If the prices jumped by 60%, and now the shelves were full of an abundance of expensive eggs, that would be suggestive that the reason for the spike in price is pure profiteering.

Price gouging, one form of profiteering [1], “is the practice of increasing the prices of goods, services, or commodities to a level much higher than is considered reasonable or fair.” [2]. The ability to sell product has nothing to do with price gouging.

Cal-Maine’s profit margin is up 7,890% year-to-year [3]. This is textbook profiteering.

>And those who have the ability to procure more eggs will now be able to demand more resources for those eggs.

What one can do is rarely what one should do. The people who can’t afford eggs could resort to violence. But where would society be then?

>or instead of requiring people to burn time and gas looking for eggs while the price of the eggs they find remains the same.

Or, like with toilet paper, meat, or several other essential items during the pandemic, groceries limit the amount of eggs customers can purchase to keep them stocked.

All this to say: We’re being fucked.

[1] https://en.m.wikipedia.org/wiki/Profiteering_(business) [2] https://en.m.wikipedia.org/wiki/Price_gouging [3] https://www.google.com/finance/quote/CALM:NASDAQ?sa=X&ved=2a...

>Egg supply is down

Egg production fell 6.6% [1]. Egg prices rose 60%.

The author knows exactly how markets work: Prices are high because there is not enough competition. Cal-Maine is tricking people into tolerating higher prices by loudly complaining about every small problem they face. They're literally bragging about it on investor calls.

[1] https://www.cnbc.com/2023/01/23/high-egg-prices-due-to-a-col...

This is not a completely hashed-out thought. But I'll share it and see what others think.

My impression is that the simplest way to improve energy efficiency is to simplify hardware. Silicon is spent isolating software, etc. Time is spent copying data from kernel space to user space. Shift the burden of correctness to compilers, and use proof-carrying code to convince OSes a binary is safe. Let hardware continue managing what it's good at (e.g., out-of-order execution.) But I want a single address space with absolutely no virtualization.

Some may ask "isn't this dangerous? what if there are bugs in the verification process?" But isn't this the same as a bug in the hardware you're relying on for safety? Why is the hardware easier to get right? Isn't it cheaper to patch a software bug than a hardware bug?

I do agree. But being able to combine old ideas in new ways is also intelligence. LLMs have memorized a ton of information, and learned “information combinators” to compose them. All that’s missing is a clean way for LLMs to engage in the scientific method.

When I ask the question, what I really mean is ``is there a mechanical structure that guarantees the correct output?'' For example, we can train neural networks to perform functions such as "and", "xor", etc., and convince ourselves the network has "really learned" what it means to calculate the function.

Is that true for interpreting programming languages? If so, a bug isn't just ``I haven't seen a similar enough example''. It reflects a deeper mistake that will likely occur again.

Is it wise to compare spending within defense budgets between these countries? Much AI research in the US is conducted by private firms. How does the current defense budget compare to historical defense budgets, such as during the early days of the digital computer in the Cold War?

On a related note: yes, Chinese researchers have models that perform certain tasks well. But are those models useful in the contexts the author mentions?

To be sure, I don't disagree that AI research needs funded. I'm just genuinely curious about these points.

I switched from Firefox to Chrome several years ago. After the announcement of the planned changes, I tried switching back to Firefox. I just couldn't stick with it -- Chromium-based browsers are faster (e.g., [1]).

I decided to give Brave a try because it's Chromium-based. It's been great. I did have to modify a few settings to get the look/feel how I like, but it I found it easy, and I expect others may not care. Brave shields block ads without the need of extensions like ublock. I don't have any complaints so far.

[1] https://www.phoronix.com/news/Firefox-95-Chrome-97

There is a funny notion that professors work for students. They don't. They hardly even work for the university. It is more correct to say that they are affiliated with the university.

At top universities, professors bring in grant money or else they lose their job. The university takes a portion of the grant before any of the money is spent. Then, the professor pays the university from the remaining money for their graduate student's tuition and stipend, to use university technology, and rent for research space. Next, the university only pays professors for 9 months out of the year. So, another chunk of grant money finances the professor's salary for the remaining 3 months.

Top universities scrape billions off research grants annually. These grants are won by faculty members. They dwarf salaries. Faculty members bring in more cash to the university than their salaries are worth.

In reality, professors finance the university. Students are mistaken if they think they are their professor's employer.

I am unable to reproduce work in CS most of the time. In part, because technology moves so fast. You can’t earn a PhD or tenure by maintaining open source software, so after a few years most implementations are rotten. Research software rots faster than other software because it’s built by people who aren’t professional engineers. Code quality doesn’t earn PhDs or tenure, either. We also use expensive new technologies with changing interfaces. So research software almost always rots.

Also in part because papers are “dressed up.” That’s a polite way of saying that the description of what they’ve built has been stretched. Authors need to make reviewers excited. They do this with ideas, not code. The purpose of their code is to show that the ideas could be practical, not that they are. So research software is almost always incomplete.

It's not necessarily about the machine's raw performance, but capacity. The compute is a shared utility, and the utilization of supercomputer is quite high. We expect science to grow exponentially. So, compute demand grows exponentially too. The cloud is crazy expensive compared to supercomputing -- you don't want missing compute to hold back research.