matu3ba

> Engineering isn't free, models tend to grow obsolete as the price/capability frontier advances, and AI specialists are less of a commodity than AI inference is. I'm inclined to bet against approaches like this on a principle.

This does not sound like it will simplify the training and data side, unless their or subsequent models can somehow be efficiently utilized for that. However, this development may lead to (open source) hardware and distributed system compilation, EDA tooling, bus system design, etc getting more deserved attention and funding. In turn, new hardware may lead to more training and data competition instead of the current NVIDIA model training monopoly market. So I think you're correct for ~5 years.

The ideas sound intriguing at first sight, so I have some questions: 1 Do you have a mathematical formalization and/or why not (yet)? 2 What would be necessary as data/proof to indicate/show either result? 3 Did you try to apply probabilistic programming (theories) to your theory? 4 There is probablistic concolic execution and probablistic formal verification. How do these relate to your theory?

Sorry, it's 4am and I should sleep, but got very interested. Thank you very much for the excellent overview. This explains all my current questions.

1 Does this mean that Sledgehammer and Coqhammer offer concolic testing based on an input framework (say some computing/math system formalization) for some sort of system execution/evaluation or does this only work for hand-rolled systems/mathematical expressions?

Sorry for my probably senseless questions, as I'm trying to map the computing model of math solvers to common PL semantics. Probably there is better overview literature. I'd like to get an overview of proof system runtime semantics for later usage. 2 Is there an equivalent of fuzz testing (of computing systems) in math, say to construct the general proof framework? 3 Or how are proof frameworks (based on ideas how the proof could work) constructed? 4 Do I understand it correct, that math in proof systems works with term rewrite systems + used theory/logic as computing model of valid representation and operations? How is then the step semantic formally defined?

> we could design something faster, safer, overall simpler, and easier to program

I do remain doubtful on this for general purpose computing principles: Hardware for low latency/high throughput is at odds with full security (absence of observable side-channels). Optimal latency/throughput requires time-constrained=hardware programming with FGPAs or building hardware (high cost) usually programmed on dedicated hardware/software or via things like system-bypass solutions. Simplicity is at odds with generality, see weak/strong formal system vs strong/weak semantics.

If you factor those compromises in, then you'll end up with the current state plus historical mistakes like missing vertical system integration of software stacks above Kernel-space as TCB, bad APIs due to missing formalization, CHERI with its current shortcomings, etc.

I do expect things to change once security with mandatory security processor becomes more required leading to multi-CPU solutions and potential for developers to use on the system complex+simple CPUs, meaning roughly time-accurate virtual and/or real ones.

> The second is that there isn’t strong demand.

This is not true for virtualization and security use cases, but not that obvious yet due to missing wide-spread attacks, see side-channel leaks of cloud solutions. Take a look at hardware security module vendors growth.

The blog looks nice, especially having simple to understand numbers. To me the memory subsystem articles are missing the more spicy pieces like platform semantics, barriers, de-virtualization (latter discussed in an article separate of the series). In the other articles I'd also expect debugging format trade-offs (DWARF vs ORC vs alternatives), virtualization performance and relocation effects briefly discussed, but could not find them. There are a few C++ article missing: 1. cache-friendly structures in C++, because standard std::map etc are unfortunately not written to be cache-friendly (only std::vector and std::deque<T> with high enough block_size), ideally with performance numbers, 2. what to use for destructive moves or how to roll your own (did not make it into c++26).

> I still think sans-io at the language level might be the future, but this isn't a complete solution. Maybe we should be simply compiling all fns to state machines (with the Rust polling implementation detail, a sans-io interface could be used to make such functions trivially sync - just do the syscall and return a completed future).

Can you be more specific what is missing in sans-io with explicit state machine for static and dynamic analysis would not be a complete solution? Serializing the state machine sounds excellent for static and dynamic analysis. I'd guess the debugging infrastructure for optimization passes and run-time debugging are missing or is there more?

I like the idea of voluntary thinking very much, but I have no idea how to properly formalize or define it.

> I mean, we've proven that predicting certain things (even those that require nothing but deduction) require more computational resources regardless of the algorithm used for the prediction.

I do understand proofs as formalized deterministic action for given inputs and processing as the solving of various proofs.

> Formalising a process, i.e. inferring the rules from observation through induction, may also be dependent on available computational resources.

Induction is only one way to construct a process and there are various informal processes (social norms etc). It is true, that the overall process depends on various things like available data points and resources.

> I don't have one except for "an overall quality of the mental processes humans present more than other animals".

How would your formalize the process of self-reflection and believing in completely made-up stories of humans often used as example that distinguishes animals from humans? It is hard to make a clear distinction in language and math, since we mostly do not understand animal language and math or other well observable behavior (based on that).

My definition of intelligence is the capability to process and formalize a deterministic action from given inputs as transferable entity/medium. In other words knowing how to manipulate the world directly and indirectly via deterministic actions and known inputs and teach others via various mediums. As example, you can be very intelligent at software programming, but socially very dumb (for example unable to socially influence others).

As example, if you do not understand another person (in language) and neither understand the person's work or it's influence, then you would have no assumption on the person's intelligence outside of your context what you assume how smart humans are.

ML/AI for text inputs is stochastic at best for context windows with language or plain wrong, so it does not satisfy the definition. Well (formally) specified with smaller scope tend to work well from what I've seen so far. Known to me working ML/AI problems are calibration/optimization problems.

What is your definition?

Can you recommend a more factual and complete overview on Apple security architecture and bootchain than this bug-ridden article? I'm interested in hardware security (models).