Loq · HackerTrans

3 yıl öncediscuss

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: https://blog.regehr.org/archives/1687

Loq

3 yıl öncediscuss

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.

Loq

3 yıl öncediscuss

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 compiler support and facilitate other RISC-V extensions, like RISC-V Vector Crypto, also to progress.

Loq

3 yıl öncediscuss

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

Loq

3 yıl öncediscuss

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

Loq

3 yıl öncediscuss

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.

[1] https://en.wikipedia.org/wiki/Railway_town

[2] https://pedestrianobservations.com/2017/09/07/meme-weeding-l...

Loq

3 yıl öncediscuss

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.

Loq

3 yıl öncediscuss

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

Loq

3 yıl öncediscuss

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

Loq

3 yıl öncediscuss

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.

Loq

3 yıl öncediscuss

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.

Loq

3 yıl öncediscuss

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.

Loq

3 yıl öncediscuss

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 constructions: Coquand/Huet (1988)

HKTs: Girard (1971)

Type classes: Kaes (1988)

Dates are imprecise and from memory.

Loq

3 yıl öncediscuss

Unlike Graal/Truffle, PyPy was done by a very small team.

Loq

3 yıl öncediscuss

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.

Loq

6 yıl öncediscuss

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

Loq

6 yıl öncediscuss

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 each other, in order to get weapons etc. Erdogan in Turkey has been masterfully doing some variation of this for a while.

Loq

6 yıl öncediscuss

    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 societies they created were worse than those that they overturned, and much worse than the best functioning societies at the time.

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.

Loq

6 yıl öncediscuss

   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, 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 ...?

Loq

6 yıl öncediscuss

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.

comments