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. Apropos:…
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.…
The official formal specification of the Vector Extension has just been merged into the Golden RISC-V model: https://github.com/riscv/sail-riscv/commit/c90cf2e6eff5fa4ef... I expect that this will help stabilise…
If you want to understand Kant in the language of (self-supervised) machine learning, I can highly recommend this rather astonishing PhD thesis: https://www.doc.ic.ac.uk/~re14/Evans-R-2020-PhD-Thesis.pdf
> loose specification of the RISC-V ISA. 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…
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…
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.…
> Is there a source for that narrative? 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…
> Is there a source for that narrative? 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…
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.…
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…
It's just a theorem prover. 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.
Dependent types: de Brujin (1967) Curry-Howard: Curry (1934, 1958), Howard (1968) MLTT: Martin-Lof (1972) Polymorphic lambda-calculus: Girard (1972/3), Reynolds (1974) Effect systems: Gifford/Lucassen (1986) Calculus of…
Unlike Graal/Truffle, PyPy was done by a very small team.
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,…
Pol Pot, Mao, Stalin ... made similar promises. Did they deliver? Political movements cannot meaningfully be evaluated by what they promise, for the all promise the world, but by - Before they come to power: by what…
That would be misleading, since it would distract attention away from the core reasons of such conflicts. Aside, during the cold war, many leaders in developing countries played the US and the Soviet union off against…
communists will tell you the soviet ideology wasn't communism. This falls in no-true-Scotsman territory, and should be seen as a self-exculpatory narrative, after all, they sent millions to an early death, yet the…
successful socialist country Does such a thing exist? What do you count as success? Just a few years earlier, and driven by the same socialist expansion strategy, another developing state turned socialist, Cambodia,…
Almost everything I know about the world, I learned through consuming mass media. One of the things I learned from the mass media is that the mass media cannot be trusted.
Everybody lies about two things: money and sex! I can't recall who said this to me as a teenager, but at the time it felt wrong! I had not yet much experience with either. Navigating the adult world changed that, but I…
The article you cite does not claim that the Navalny poisoning was a US/Saudi false flag. On the contrary, Murry states: "I should state that I have no difficulty at all with the notion that a powerful oligarch or an…
Murray did not state that Skripal was a false-flag by the UK government. He did ask several questions about the nature of the official UK government's explanation which you find at [1]. Can you point me towards credible…
moving towards a compiler approach. What do you mean by "compiler approach" in this context?
Most of Taiwan is fairly mountainous and empty. Most of the population is in a few cities (Kaohsiung Taichung Tainan Taipei Taoyuan). It's enough to connect them with high-speed trains, and that's what happened.
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. Apropos:…
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.…
The official formal specification of the Vector Extension has just been merged into the Golden RISC-V model: https://github.com/riscv/sail-riscv/commit/c90cf2e6eff5fa4ef... I expect that this will help stabilise…
If you want to understand Kant in the language of (self-supervised) machine learning, I can highly recommend this rather astonishing PhD thesis: https://www.doc.ic.ac.uk/~re14/Evans-R-2020-PhD-Thesis.pdf
> loose specification of the RISC-V ISA. 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…
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…
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.…
> Is there a source for that narrative? 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…
> Is there a source for that narrative? 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…
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.…
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…
It's just a theorem prover. 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.
Dependent types: de Brujin (1967) Curry-Howard: Curry (1934, 1958), Howard (1968) MLTT: Martin-Lof (1972) Polymorphic lambda-calculus: Girard (1972/3), Reynolds (1974) Effect systems: Gifford/Lucassen (1986) Calculus of…
Unlike Graal/Truffle, PyPy was done by a very small team.
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,…
Pol Pot, Mao, Stalin ... made similar promises. Did they deliver? Political movements cannot meaningfully be evaluated by what they promise, for the all promise the world, but by - Before they come to power: by what…
That would be misleading, since it would distract attention away from the core reasons of such conflicts. Aside, during the cold war, many leaders in developing countries played the US and the Soviet union off against…
communists will tell you the soviet ideology wasn't communism. This falls in no-true-Scotsman territory, and should be seen as a self-exculpatory narrative, after all, they sent millions to an early death, yet the…
successful socialist country Does such a thing exist? What do you count as success? Just a few years earlier, and driven by the same socialist expansion strategy, another developing state turned socialist, Cambodia,…
Almost everything I know about the world, I learned through consuming mass media. One of the things I learned from the mass media is that the mass media cannot be trusted.
Everybody lies about two things: money and sex! I can't recall who said this to me as a teenager, but at the time it felt wrong! I had not yet much experience with either. Navigating the adult world changed that, but I…
The article you cite does not claim that the Navalny poisoning was a US/Saudi false flag. On the contrary, Murry states: "I should state that I have no difficulty at all with the notion that a powerful oligarch or an…
Murray did not state that Skripal was a false-flag by the UK government. He did ask several questions about the nature of the official UK government's explanation which you find at [1]. Can you point me towards credible…
moving towards a compiler approach. What do you mean by "compiler approach" in this context?
Most of Taiwan is fairly mountainous and empty. Most of the population is in a few cities (Kaohsiung Taichung Tainan Taipei Taoyuan). It's enough to connect them with high-speed trains, and that's what happened.