Re: [Axiom-developer] AI is coming for my job!

I would venture the proofs are not the real effort in CompCert.

The real effort is to formulate the various systems such that the

proofs become as simple as possible. So 15.77% is minuscule

compared to the total intellectual effort of this project. Your job

is not yet in danger (even in your retirement :-)

But, seriously, sometimes I am worried that too much automation

is a bad thing, because it can mask the flaws in what one is doing.

There are many examples in the study of logics, but let me use

programming instead. Start with your favorite terrible programming language

(Python happens to be a convenient target, or C++). Now, sure, you can

reduce the number of bugs with automatic program analysis, the smarter

the better. But you would nevertheless still be better off in a statically typed

functional language with a decent module system. You prop up something

that would be better left to wither and die.

- Frank

On Sun, Jul 21, 2019 at 8:29 AM Tim Daly <address@hidden> wrote:

Generating Correctness Proof with Neural Networks
https://arxiv.org/pdf/1907.07794.pdf

Apparently they managed to prove 15.77% of the proofs in
the CompCert verified compiler effort.

"Now, here, you see, it takes all the running you can do to
keep in the same place. If you want to get somewhere else,
you must run at least twice as fast as that."
-- Alvin Toffler "Future Shock" :-)

Tim

From:	Frank Pfenning
Subject:	Re: [Axiom-developer] AI is coming for my job!
Date:	Sun, 21 Jul 2019 10:35:56 -0400