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.
122 karma · joined May 3, 2019
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.
https://github.com/riscv/sail-riscv/commit/c90cf2e6eff5fa4ef...
I expect that this will help stabilise compiler support and facilitate other RISC-V extensions, like RISC-V Vector Crypto, also to progress.
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.
[1] https://github.com/riscv/sail-riscv
[2] https://github.com/riscv/sail-riscv/blob/master/model/riscv_...
[1] https://en.wikipedia.org/wiki/Railway_town
[2] https://pedestrianobservations.com/2017/09/07/meme-weeding-l...
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.
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.
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.
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 constructions: Coquand/Huet (1988)
HKTs: Girard (1971)
Type classes: Kaes (1988)
Dates are imprecise and from memory.
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 they are likely to deliver (which is predicted from what similar policies have lead to in the past).
- Post facto: what they did deliver.
This is obvious. Everybody in this discussion is aware of this.
There is an interesting social phenomenon at play here, that deserves intellectual curiosity and explanation: there is no identifiable political ideology in the history of humanity that failed to deliver so hard and so often with identical policies, as the Marxist position via Leninist cadre parties. Yet even today, we we see apologias like pjc50's despite Marxist / Leninist cadre parties. I've even pointed to the A/B testing that were the division of Germany and Korea.
Many times people have tried to answer this question. I'm broadly in agreement with Nietzsche on this one ...
Aside, during the cold war, many leaders in developing countries played the US and the Soviet union off against each other, in order to get weapons etc. Erdogan in Turkey has been masterfully doing some variation of this for a while.
communists will tell you
the soviet ideology wasn't
communism.
Let's also be clear that Soviets read the works by Marx and Engels in great detail, it's not like they didn't know what Marx and Engels wrote. For example, the Communist Manifesto [1, 2] outlines a few essential demands [3] for a transition that will eventually lead to communist utopia. Every single one of those was executed, and achieved by Stalin.
Exactly what "communism" should mean has never really been clarified, but whatever Marx and Engels meant by it, the fact that carrying out their 10 key demands exacted an 8 digit death toll is an extremely strong indication that there is something fundamentally wrong with Marx and Engels ideas.
Moreover, the world A/B tested this: two countries were split (Germany and Korea), one was ruled by a communist party (Soviet aligned) the other capitalist and within a decade the capitalist one was doing dramatically better than the other. So much so, that you Soviet aligned one had to turn itself to a prison to prevent the population from fleeing. (Yes I am aware that this is not a repeatable scientific experiment. However it is the most decisive 'experiment' you can hope for in politics and social theory. It is what we must learn from. To quote Marx: "A Nation should and can learn from other nations".)
[1] K. Marx, F. Engels, Manifesto of the Communist Party. http://activistmanifesto.org/assets/original-communist-manif...
[2] https://en.wikipedia.org/wiki/The_Communist_Manifesto
[3] Briefly (and from [2]): progressive income tax; abolition of inheritances and private property; abolition of child labour; free public education; nationalisation of the means of transport and communication; centralisation of credit via a national bank; expansion of publicly owned land, etc.—the implementation of which would result in the precursor to a stateless and classless society.
successful socialist country
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, with active help from Moscow. Is this what you have in mind as success?
Wasn't Sankara a charismatic leader, and military man who came to power by a coup d'état? Have you looked at the track record of military coup d'états in history ...?
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 didn't grow beyond a vague feeling of the need for caution in delicate human matters. It was only when I learned about crypography, security and distributed systems, that I understood the value, and indeed necessity, of having attacker models. I realised that the social world, too, has benign and adversarial parts (and many shades inbetween): for example you can trust your mathematics teachers nearly 100% when they talk about mathematics, but you should probably be prepared for being taken advantage off in financial transactions, whence the aphorism.
The article states that "[T]he US and Saudi Arabia have every reason to instigate a split between Germany and Russia at this time." The US has gone out of the way to prevent the NordStream 2 pipeline, and directly after Navalny was flown to Germany, several high-ranking German politicians (including Merkel), have began publicly to question whether NordStream 2 should be reconsidered, in the light of Navalny, see [1].
May I gently request that you exercise more care when representing Murray's views? Please reconsider the HN guidelines for comments [2], reproduced here for your convenience: "Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize. Assume good faith."
Can you point me towards credible answers to some / all the questions raised in [1] please?
[1] https://www.craigmurray.org.uk/archives/2019/03/pure-ten-poi...
moving towards a compiler
approach.
... 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. Somebody else abused your trust by talking to HR, hence you could decide on the simple policy of never trusting them again, and cut them out of your high-trust network. Some fail your trust-related tests, some pass. Use this information wisely. (Note that an alternative policy is not being too history-sensitive, and let bygones be bygones.)
Incidentally, the essence of what you say (the mind is always predicting and learns from prediction failure) is also the essence of idealist philosophy, and has found its most advanced expression in Kant's Critique of Pure Reason. Unfortunately, Kant uses a language that's difficult to access today, so a lot Kant's insight has fallen out of today.
Note also that pretending to drink feels a bit like cheating to me: I'm actively deceiving others. I wish I could live my life without deceit.
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 latter option engenders trust.
"I don't trust someone that I didn't get drunk with" is a sentiment I've heard repeatedly, both privately and professionally. The most successful startup that I worked for even asked "What's your favourite beer?" when they interviewed me for a programmer position, and when I asked by this was of interest, they said they took their after work drinking sessions pretty seriously, and "don't want to work with people they can't have fun with". As somebody who doesn't enjoy being drunk, this was difficult for me to adapt to.