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.

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?

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.

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.

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

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?

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.

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.

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?