<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Nicolas, are you aware of SAT-SMT solvers? (<a href="https://sat-smt.codes/SAT_SMT_by_example.pdf">SAT/SMT by Example (sat-smt.codes)</a>) Microsoft used Z3 to great effect in flushing out bugs in Vista. SAT-SMT's used in a thing called <a href="https://en.wikipedia.org/wiki/Concolic_testing">Concolic testing - Wikipedia</a>,</div><div dir="ltr"><br></div><div>frank</div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 17 May 2021 at 05:14, Nicolas Cellier <<a href="mailto:nicolas.cellier.aka.nice@gmail.com">nicolas.cellier.aka.nice@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">More seriously, there is not a single kind of test.<br>
One category is kind of specification illustrating the expectations,<br>
and demonstrating how to use some message/class.<br>
Most of the time, our tests as specification lack the quantifiers<br>
(like the universal quantifier), that's why I name them illustrating.<br>
Ideally, we would like to have some form of formal proof, but there<br>
rarely is one accessible, unless we drastically restrict the<br>
capabilities (like recursivity and all forms of reflexivity)<br>
At least, that's my understanding of<br>
<a href="https://en.wikipedia.org/wiki/Formal_methods" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Formal_methods</a><br>
<br>
In some rare cases, we now have enough computing power to test an<br>
implementation exhaustively (like a function of a single float32<br>
argument).<br>
Alternatively, we can try and test with randomly generated inputs, but<br>
that's a bit like shooting in the dark.<br>
<br>
In order to be more eager, we sometimes write tests against a specific<br>
implementation with specially crafted examples for non regression or<br>
main gotchas of the specific algorithm.<br>
I guess my efforts fall in such a category: it's kind of adversarial<br>
strategy; somehow like a game of finding the shortcomings.<br>
If we have watts to burn, I think that it would be interesting to use<br>
machine power to find and construct those adversarial examples, not<br>
based on sole randomness, but some form of analysis of algorithms and<br>
probably some set of heuristics.<br>
How could we build such machinery, I don't know, for now it's still buzzwords.<br>
<br>
Le lun. 17 mai 2021 à 12:00, Nicolas Cellier<br>
<<a href="mailto:nicolas.cellier.aka.nice@gmail.com" target="_blank">nicolas.cellier.aka.nice@gmail.com</a>> a écrit :<br>
><br>
> Le dim. 16 mai 2021 à 17:10, David T. Lewis <<a href="mailto:lewis@mail.msen.com" target="_blank">lewis@mail.msen.com</a>> a écrit :<br>
> ><br>
> > On Fri, May 07, 2021 at 07:39:50PM +0000, <a href="mailto:commits@source.squeak.org" target="_blank">commits@source.squeak.org</a> wrote:<br>
> > > Nicolas Cellier uploaded a new version of Kernel to project The Trunk:<br>
> > > <a href="http://source.squeak.org/trunk/Kernel-nice.1402.mcz" rel="noreferrer" target="_blank">http://source.squeak.org/trunk/Kernel-nice.1402.mcz</a><br>
> > ><br>
> > ><br>
> > > Musing is more powerful than dumb static and coverage tests, I wish I got more time for musing :)<br>
> > > We deadly need evolutive testing (neural based).<br>
> > ><br>
> ><br>
> > Interesting commit comment. How might this work?<br>
> ><br>
> > Dave<br>
> ><br>
> ><br>
> Hi Dave,<br>
> How? This way: put enough buzzwords in commit comments to bring some<br>
> academics on the subject ;)<br>
<br>
</blockquote></div>