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

[Jeffrey Shallit]

Unfortunately no one is going to pay for that!

On 2022-10-21 3:01 PM, Neil Sloane wrote:
> "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/
>>
> --
> Seqfan Mailing list - http://list.seqfan.eu/