Loq

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.

While the likes of Zuse and Flowers deserve more recognition, here are some other of Turing's achievements.

- Introduced the concept of ordinal logic, an apporach to overcoming the limitations of Goedel's incompleteness theorems, a thriving field as of 2019. See [1].

- Gave the definite analysis of the notion of "mechanical computability", see [2].

- Essentially invented the field of AI, with key contributions such as Neural Networks [3] (but see [4, 5, 9]) and the Turing test [6].

- Work in chemistry / biology, see [7, 8].

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

[2] https://en.wikipedia.org/wiki/Turing_machine

[3] https://www.info2007.net/docs/intelligent-machinery-alan-tur...

[4] http://compucology.net/unorganized

[5] http://compucology.net/criticism

[6] https://en.wikipedia.org/wiki/Turing_test

[7] http://www.dna.caltech.edu/courses/cs191/paperscs191/turing....

[8] https://arstechnica.com/science/2018/05/alan-turings-contrib...

[9] http://www.alanturing.net/turing_archive/pages/Reference%20A...

ILP usually translates to SAT. You can see ILP as a high-level interface to SAT.

Thanks.

Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.

Have those handwritten proofs been published?

BTW, has CryptoVerif been proven sound? I.e. has it been shown that the game transformations CryptoVerif produces really only amount to negligible probability transformations?

   “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 calculi).

CryptoVerif outputs what might be seen as program transformations:

   P = Q

such that the probability that a polynomially bounded adversary can 'crack' P is only negligibly different from the probability for Q. This can be seen as a probabilistic generalisation of e.g. the program transformations that an optimising compiler does, except that in compilation you need that P and Q have exactly the same (observable) behaviour.

Verifying crypto protocols is essentially the production of a chain

   P1 = P2 = ... = Pn

where P1 is the protocol in question, and Pn is some "obviously secure" protocol (e.g. existence of one-way functions). Note that Pn might be doing something different from P1. What's important is that the probabilities remain 'similar' (this can be made precise). This proves that P1 is as secure as Pn, so we can break the latter if we can break the former.

The reason for the "game" terminology is historical. Von Neumann's theory of economic games [1] preceeds the development of programming languages for interactive behaviour [2] by many decades.

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

[2] https://en.wikipedia.org/wiki/Process_calculus

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 that compilers obtained from interpreters by Futamura didn't perform well. Indeed, in his 2010 PEPM keynote, Augustsson asked: "O, partial evaluator, where art thou?" [1]

Is there a brief summary what is Graal etc doing differently to overcome 1990s style partial evaluation performance problems?

[1] https://dl.acm.org/citation.cfm?id=1706356.1706357

   These aren't indicators 
   of lack of trust

I disagree. There are multiple levels of trust:

- Your partner that they don't lie about taking contraception, that they have taken it as required.

- The medical sciences and medical regulatory authorities that the contraception works as expected.

- Pharmacist that they don't sell counterfeit medicine

and many others. Society is largely based on trust.

Clearly A's statement

   I'm using contraception method X

could be true or false. If you are not verifying the truth of this statement, and have heterosexual intercourse with A, you are trusting A. How do you verify such a statement in practise?

    potentially decades away   

Would you be able to sketch, in a sentence or two, why we can be reasonably certain about cures being difficult. Is there a specific reason? Are you similarly pessimistic about a vaccine?

The demand for Levonorgestrel (aka Plan B, or morning-after pill), abortion, not to mention other STDs, can be seen as indicating that that trust is not always warranted.