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.…
> 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…
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? 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,…
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.
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…
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.
This is true, but ... ... you can analyse this in a different way: think long term! The more successful you are in your job, the more you will bump into the same people again and again later, sometimes a decade later.…
I agree with you, in that pretending to drink (e.g Tonic instead of Gin & Tonic) is probably what a lot of us do, and the obvious way out. But the point of drinking is not really being sociable, but making yourself…
one reason I do like working remote is that I don't have to deal with others' grade 8 drama skills!
Could you give an example? The most popular trust-creation mechanism for adults seems to be getting drunk together, which reliably leads to little infractions, which every witness has the choice to exploit or not. The…
Would you be able to sketch what makes PyTorch better than TF? And maybe why Google are sticking with TF -- it's not like Google lack technical ability to do / copy what PyTorch does.
No. I meant was ASP is a higher level 'interface' to SAT, sorry for the confusion. Work done at Imperial by Law and Evans in ILP compiles down to SAT solving via ASP. IDK if δILP goes to SAT.
ILP usually translates to SAT. You can see ILP as a high-level interface to SAT.
“Games” are a ... I think the terminology of games is a bit misleading. A better term would be program but in a (probabilistic) programming language that specifies interaction by message passing (such as process…
There was a lot of work on partial evaluation in the 1990s, including getting compilers via Futamura. But that research mostly withered. Speaking to some the old timers, I get the impression that the core problem was…
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.…
> 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…
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? 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,…
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.
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…
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.
This is true, but ... ... you can analyse this in a different way: think long term! The more successful you are in your job, the more you will bump into the same people again and again later, sometimes a decade later.…
I agree with you, in that pretending to drink (e.g Tonic instead of Gin & Tonic) is probably what a lot of us do, and the obvious way out. But the point of drinking is not really being sociable, but making yourself…
one reason I do like working remote is that I don't have to deal with others' grade 8 drama skills!
Could you give an example? The most popular trust-creation mechanism for adults seems to be getting drunk together, which reliably leads to little infractions, which every witness has the choice to exploit or not. The…
Would you be able to sketch what makes PyTorch better than TF? And maybe why Google are sticking with TF -- it's not like Google lack technical ability to do / copy what PyTorch does.
No. I meant was ASP is a higher level 'interface' to SAT, sorry for the confusion. Work done at Imperial by Law and Evans in ILP compiles down to SAT solving via ASP. IDK if δILP goes to SAT.
ILP usually translates to SAT. You can see ILP as a high-level interface to SAT.
“Games” are a ... I think the terminology of games is a bit misleading. A better term would be program but in a (probabilistic) programming language that specifies interaction by message passing (such as process…
There was a lot of work on partial evaluation in the 1990s, including getting compilers via Futamura. But that research mostly withered. Speaking to some the old timers, I get the impression that the core problem was…