[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut

[Neil Sloane]

"Program verification" has been big business for decades: several of my
former colleagues at Bell Labs spent their whole careers working on this
problem - and founded companies to do it commercially.  Someone should get
"Walnut" professionally certified.  You have to start with a detailed
specification of what Walnut is supposed to do, but that must already exist.

Best regards
Neil

Neil J. A. Sloane, Chairman, OEIS Foundation.
Also Visiting Scientist, Math. Dept., Rutgers University,
Email: njasloane at gmail.com



On Fri, Oct 21, 2022 at 11:55 AM <hv at crypt.org> wrote:

> Jeffrey Shallit <shallit at uwaterloo.ca> wrote:
> :In case you missed the talk, it is now available at
> :
> :https://cs.uwaterloo.ca/~shallit/walnut.html
>
> Thanks for sharing the video - I had hoped to attend the talk, but was
> unable to make it.
>
> I'm especially glad that Neil asked what it means to say that Walnut
> is "proving" a theorem - the same question occurred to me very early
> in the talk.
>
> I think your analogy of primality tests is quite relevant, in particular
> because we _can_ provide a certificate of primality that can be verified
> much more quickly than testing ab initio. This analogy also holds
> particular resonance for me: on several occasions I've had to repeat
> calculations after discovering bugs that affected number theory software
> libraries on which I had relied.
>
> On one occasion I had to redo about two years' worth of calculations
> after finding a bug in the factorization of numbers between 2^63 and
> 2^64 in size - luckily this coincided with the acquisition of a new
> computer, and I was able to complete the recalculations in a mere
> couple of months; I remain anxious that one day I'll find another
> problem that cannot be remedied so quickly.
>
> While I know a little about DFAs from my programming work (including
> a lot of work on the regexp engine in Perl), I know little about them
> mathematically. Is it plausible that Walnut could generate a kind of
> certificate by outputting one or more DFAs along with some
> canonicalized description of the transformations it is performing
> on them?
>
> It is a fact of life that software will have bugs, and it is always
> important to think what we can do to mitigate the effect of them.
> Creating some sort of breadcrumb trail to allow for verification
> seems highly worthwhile if the potential risk is that we think we've
> proved something that turns out not to be true.
>
> Hugo van der Sanden
>
> --
> Seqfan Mailing list - http://list.seqfan.eu/
>