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.

>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.