Indeed, what bqmjjx0kac proposes, is orthogonal to fuzzing (which is an algorithmic technique to drive test-coverage), and an instance of defining, and dynamically checking a property.
Fuzzing and constrained random, while both based on randomisation, are not the same thing.
A big problem of fuzzers from the point-of-view of hardware validation is that it's unclear what coverage guarantees they give. Would you tape out your processor design, once your fuzzer no longer finds bugs, if you had no idea about test coverage? OTOH, fuzzing has been very effective in software, so it is natural to ask if those gains can also be had for hardware.
This is being worked on with the Sail model [1]. In order for a RISC-V extension to be ratified it ought to be implemented in Sail. The understanding is also that the RISC-V ISA manual should be built with code snippets from the Sail model (similar to how the Arm ARM is build from ASL definition). The main issue is a lack of people willing and able to write Sail for RISC-V. But that is beginning to change, since RISC-V member companies are increasingly use Sail. As an example, the RISC-V exception type is defined in [2]. Is that precise enough for you?
The formal RISC-V ISA specification is not finished, you are welcome to make a PR to clarify things.
This is a much older phenomenon, called railway town, and it is so frequent that it has its own Wikipedia page [1]. At smaller scale this also happens in cities where new underground lines are built. It's a well-established way of paying for public transport. See [2] for a discussion.
Turing award winner Dana Scott already mentions categories in his work on models for the untyped lambda-calculus, for example in his 1971 monograph on Continuous Lattices, which set the foundations of domain theory. Moggi monads came about, in parts, as a way of understanding domain theoretic constructins better.
Girard mentions the connection with categories all the time.
For example in "Proofs and Types"
he proves various theorems along the lines of: the sub-category of coherence spaces and stable maps (one of the main models that LL was developed for) induced by some LL fragment is
cartesian closed category (IIRC). I think he developed LL in parts by fine-tuning it, until all the categories induced as models of fragments of LL have nice categorical properties. (To the extent that is possible.)
When I was a PhD student, my supervisor suggested that I learn category theory to understand linear logic. (Not sure, in retrospect, that was the best course of action, but that was my trajectory)
Rust's types evolved over many years. Rust used to have "typestate" for example. I had discussions with Graydon Hoare around 2011-ish about session types (which are linear). It struck me that Hoare knew exactly what I meant with the term. More generally, linear typing was just "in the air" in the early 2000s: you could not been serious in programming language design without being aware of linearity. Linearity was all over the research literature. Hoare was clearly very knowledgable in programming language research.
You could look at the papers being published in conferences like POPL, LICS, PLDI and ICFP.
The theory of (Moggi) monads and monad transformers has been influencing modern programming (and libraries) very heavily (e.g. all of Haskell, Scala's ZIO vs Cats, Rust approach to returning errors). Most modern programming language research engages in some form or other with linear types (and its relatives, like affine) and they come from Girard's linear logic. Both (Moggi) monads and linear logic are heavily influenced by their inventors learning of category theory. So I'd say, whenever you program in a modern language or use modern library design, you (indirectly) stand on the shoulders of many giants. Some of those giants were category theorists.
Interestingly, what I'm beginning to detect is an influence of computer science on category theory, if only because we want to verify abstract maths in automated tooling.
Category theory has been extremely influential in computer science, primarily because a (maybe the) prototypical idealised programming language (the simply typed lambda-calculus) is at the same time, a logic and a convenient syntax for cartesian closed categories (= basically the nicest, most well-behaved kind of category (which is, in turn, a foundation of topoi, a generalisation of the essence of all logics)).
The trias gives extreme scope for technology transfer between mathematics, logic and programming.
Like every theorem prover it has a logic that you use for stating propositions, and proving theorem. The logic is a specific logic that is closely related to HoTT.
Could you give me references for this theory of meta-tracing in the 1990s? It seems to me that PyPy was the first to, systematically and in a lightweight way, solve the problem of normal JITs optimising the wrong loop, when JITing interpreter loops.
Apropos: https://blog.regehr.org/archives/1687