[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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

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

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


Frank Pfenning, Professor
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213-3891

+1 412 268-6343
GHC 6017

reply via email to

[Prev in Thread] Current Thread [Next in Thread]