[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut
njasloane at gmail.com
Fri Oct 21 21:01:12 CEST 2022
"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.
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
> 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/
More information about the SeqFan