madmax96 · HackerTrans

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.

madmax96

11 ay öncediscuss

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?

madmax96

2 yıl öncediscuss

Is bandwidth the limiting factor or is it ping?

madmax96

2 yıl öncediscuss

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.

madmax96

2 yıl öncediscuss

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

madmax96

2 yıl öncediscuss

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

madmax96

2 yıl öncediscuss

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

madmax96

2 yıl öncediscuss

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

madmax96

2 yıl öncediscuss

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

madmax96

10 yıl öncediscuss

Of course the selection of data is arbitrary -- but Rich gives us a definition, which he makes abundantly clear and uses consistently. All definitions can be considered arbitrary. He's not making any claim that we have all the relevant bits of data or that we can be sure what the data really means or represents.

But we can expound on this problem in general. In any experiment where we gather data, how can we be sure we have collected a sufficient quantity to justify conclusions (and even if we are using statistical methods that our underlying assumptions are indeed consistent with reality) and that we have accrued all the necessary components? What you're really getting at is an __epistemological__ problem.

My school of thought is that the only way to proceed is to do our best with the data we have. We'll make mistakes, but that's better than the alternative (not extrapolating on data at all.)

comments