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.

CHERI on its own does not fix many of the side-channels, which would need something like "BLACKOUT : Data-Oblivious Computation with Blinded Capabilities", but as I understand it, there is no consensus/infra on how to do efficient capability revocation (potentially in hardware), see https://lwn.net/Articles/1039395/.

On top of that, as I understand it, CHERI has no widespread concept of how to allow disabling/separation of workloads for ulta-low latency/high-throughput/applications in mixed-critical systems in practical systems. The only system I'm aware of with practical timing guarantees and allowing virtualization is sel4, but again there are no practical guides with trade-offs in numbers yet.

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

Sorry for necro-bumping, but there is a paper doing exactly that besides various other things to eliminate timing channels claiming also to prevent attacks based on speculative execution etc: "BLACKOUT : Data-Oblivious Computation with Blinded Capabilities" https://arxiv.org/abs/2504.14654. They basically utilize another bit of CHERI for "blinded capability" and methods to mitigate potential problems you identified.

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?

What would be more sane alternatives, when it becomes obvious that any side-effect of timing is a potential attack vector? See https://www.hertzbleed.com/ for frequency side channels. I do only see dedicated security cores as options with fast data lanes to the CPU similar to what Apple is doing with Secure Enclave or do you have better suggestions that still allow performance and power savings?

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

Forming deterministic actions is a sign of computation, not intelligence.

What computations can process and formalize other computations as transferable entity/medium, meaning to teach other computations via various mediums?

Intelligence is probably (I guess) dependent on the nondeterministic actions.

I do agree, but I think intelligent actions should be deterministic, even if expressing non-deterministic behavior.

Computation is when you query a standby, doing nothing, machine and it computes a deterministic answer.

There are whole languages for stochastic programming https://en.wikipedia.org/wiki/Stochastic_programming to express deterministically non-deterministic behavior, so I think that is not true.

Intelligence (or at least some sign of it) is when machine queries you, the operator, on it's own volition.

So you think the thing, who holds more control/force at doing arbitrary things as the thing sees fit, is more intelligent? That sounds to me more like the definition of power, not intelligence.

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

Money is created and distributed via 1 banking system and 2 government. Are 1 rules, 2 checks and 3 punishment enforced against the banking system and government or only to stabilize and extend those systems? I'd argue the introduction of (arbitrary) rules are often just the excuses to amass power, but enforcement of checks and punishments decides who holds (political) power.

Regulations are practically the only thing standing between the rich and the powerful and their incessant attempt to drive even more wealth into their own pockets at the expense ordinary people's health, wealth, future, welfare, housing, etc.

Try to rethink how money is created and how money gets its value and how and by whom that wealth is distributed. Regulation as in "make rules" does not enforce rules, which is the definition of (political) power.

The other important requirement is to increase the staffing of the regulatory agencies so that their individual workload doesn't become a bottleneck in the entire process. There is a scientific method to assess the staffing requirements of public service institutions. According to that, a significant number of government departments all over the world are understaffed.

Why are you claiming "There is a scientific method" and do not provide it? Governments do (risk) management by 1 rules, 2 checks and 3 punishment and we already know from software that complexity in system is only bounded by system working with eventual necessary (ideally partial) resets. Ideally governments would be structured like that, but that goes against governments interest of extending power/control. Also, "system working" is decided by the current ruling class/group. Besides markets and physical constrains.

Call me grumpy and sleep deprived, but every year I look at this talk again, and every year I wonder... "now, what" ? What am I supposed to do, as a programmer, to change this sad state of things ?

That depends on your goals. If you are into building systems for selling them (or production), then you are bound by the business model (platform vs library) and use cases (to make money). Otherwise, you are more limited in time.

To think more realistically about reality you have to work with, take a look at https://www.youtube.com/watch?v=Cum5uN2634o about types of (software) systems (decay), then decide what you would like to simplify and what you are willing to invest. If you want to properly fix stuff, unfortunately often you have to first properly (formally) specify the current system(s) (design space) to use it as (test,etc) reference for (partial) replacement/improvement/extension system(s).

What these type of lectures usually skip over (as the essentials) are the involved complexity, solution trade-offs and interoperability for meaningful use cases with current hw/sw/tools.

What is the most optimal Erlang/Elixir you can think of regarding standardized effect systems for recording non-determinism, replaying and reversible computing? How comparable are performance numbers of Erlang/Elixir with Java and wasm?

Author completely misunderstands how to use exceptions and is just bashing them. A lot of what he says is inaccurate if not outwardly incorrect.

Do you mind to elaborate what you believe are the misunderstandings? Examples of incorrect/inaccurate statements and/or an article with better explanations of mentioned use cases would be helpful.

it's called std::expected

How does std::expected play together with all other possible error handling schemas? Can I get unique ids for errors to record (error) traces along functions? What is the ABI of std::expected? Stable(ish) or is something planned, ideally to get something C compatible?

I do agree with point 1 and with most of point 2 besides some more arcane things like intentionally racy memory access and some write-cache eviction instruction not being properly modeled (in for example Rust).

I would expect more of the opposite for languages offering easy to enable bound checks. Only observing the general trend for when bound checks are available (and used) would be helpful information. Temporal ones will remain tricky to debug until at least static + dynamic analysis via scheduling in kernel, hypervisor/simulation and/or run-time will become common-place. Probably even longer, because analysis is cumbersome for bigger programs without Seperation Logic (like Rust has).

1 The numbers on memory safety should nowadays separate between spatial ones (bounds-checked in most languages with sane flags) and temporal ones. Temporal ones will be lower than 70%.

2 The article does not mention (compilation) time costs of static checks and its influence on growing code bases, which is a more fundamental system trade-off on scalability and development velocity/efficiency.

Wrap unsafe code with safe interfaces

3 That sounds like an equivalent of using permission-based separation logic hopefully soon available for LLVM.

"Get good" is not a strategy

4 Being good is all about knowing exactly techniques, processes, and tools with exact trade-offs and applying them; so I would expect here teaching process knowledge about static and dynamic analysis strategies, tooling and tactics to eliminate bug classes. However, neither have we sane bug classes overviews nor can we generate sane probabilities/statistics of occurrence based on source code and available static and dynamic analysis even when ignoring functionality requirements. This reads somewhat like developers should "stay mediocre" and "trust the tools", even though "Get good and improve processes for groups" is probably the here intended strategy.

Thanks. Sounds like a good developer experience attempt.

Scheduling means to generate enumerations/combinations of possible ui events. If interleaving events are possible and to what degree, then providing a notion of that and/or at least documentation would be helpful.

Yeah, although I would define "reversible computing" as how to deterministically undo some computation(s)/effect(s) etc without recording the control-flow and I do not like the notation of "time-reversibility", because distinguishing between "reversible computing with known timings" and "reversible computing with unknown timings" becomes very confusing. So I'd phrase it somewhat differently, but did not come up with better naming yet. Context: https://en.wikipedia.org/wiki/Reversible_computing and https://en.wikipedia.org/wiki/Time_reversibility.

Since you think the UI scene is maturing: Where do I find 1. design docs and 2. debugging infra docs (Validation, Testing, Stepping, Logging, Tracing, Recording, Scheduling, Reversal Computing as typical ones) and/or how to apply them ?

inherent to the problem domain that you're working with and which there is no way around for

I'd phrase it to reasonable taken trade-offs for customer/user support and/or selling products.

going for a microservices architecture when you need to serve about 10'000 clients

So far I am only aware of the use case to ship/release fast at cost of technical debt (non-synchronized master) of microservices. As I understand it, this is to a large degree due to git shortcomings and no more efficient/scalable replacement solution being in sight. Or can you explain further use cases with technical necessity?

right now I want to actually make a super easy to install memory safe sshd distro

That is amazing and looks like an excellent first use case.

Is this your last design iteration? Benchmarks would be great and some performance justification based on the design (techniques).

Are all possible memory problems checked, which to me include those listed in https://matu3ba.github.io/articles/optimal_debugging/#practi... (OOB, null, type confusion, integer overflow, invalid stack access, UUM, data races, illegal aliasing/provenance, stack overflows, ..) ?

1 Do you have benchmarks for the RISC-V "physical memory protection unit" and/or where can I read more? I'm looking ideally for things like type 1/2 hypervisor or Kernel tutorials for RISC-V to exemplify technical trade-offs. 2 Separation of virtual memory<->security sounds reasonable to offload security eventually to simpler and verified (and ideally eventually synthesized) hypervisors instead of complex Kernels, but I am wondering about capability and debugging limits. 3 The last sentence is very speculative and I dont get how that could be reached.