Indeed, the whole point is that you shouldn't add equality of functions to a language. I disagree that the formal proof of function equivalence is a red herring. Rather, it is the crux of the problem: the only sensible equality of functions turns out to be observational equality, which is non-trivial to handle. But in order to understand that, you eventually have to discuss what it would take to add such a thing to a language. Talk is rather cheap compared to writing a robust compiler with deterministic interfaces. In the same vein, I don't think float32 and float64 should be eqtypes either. Nor, can it be argued, should a map or array because their equivalence isn't an O(1) operation.
On Fri, Nov 25, 2016 at 11:38 AM 'Axel Wagner' via golang-nuts < golang-nuts@googlegroups.com> wrote: > I think, in the context of this thread, talking about formally proving > whether two functions produces equivalent results is a red herring. > > a) It is an impossible problem to solve in general, so you'd need to > restrict your definition to some provable subset > b) That will be impossible to put in a spec in any sensible way without > blowing it up immensely > c) Even if, that subset can't include side-effects, which would make it > completely useless for go > and d) even if you could, requiring to implement those proofs would make > it highly unlikely if not impossible, that more than one (or a very small > handful) go-implementation exists, defeating the point of a good spec in > the first place (think about, for example, what that would mean for > gopherjs or gomobile, where a func() can be implemented by opaque > javascript/asm/dalvik bytecode/compiled machine code). > > If you want to debate the finer points of such proof engines for go > existing as a tool separate from the language, I think that should go in a > separate thread. I don't think it can be sensibly argued that it should > become part of the language as the equality operator on func's. > > On Fri, Nov 25, 2016 at 11:05 AM, Jesper Louis Andersen < > jesper.louis.ander...@gmail.com> wrote: > > > On Fri, Nov 25, 2016 at 12:30 AM Michael Jones <michael.jo...@gmail.com> > wrote: > > This is very nice! However, am i right in understanding that the magic is > in knowing the text of the program--the fact that there are untaken > branches? If so, this is not simply a 'behavioral' verification...it knows > about the construction of the code and not just its behavior. Maybe I was > unclear. > > > > Indeed you are right. This requires the ability to work on the program > text. It is a bit too hard to work on the output assembly for the program. > The advantage of a model-checker or a probalistic method such as > "testing/quick" is that they regard the system-under-test as a black box. > > This fact can be used in numerous ways. The most powerful one is that once > you have a specification model, in *any* programming language, it applies > to any system implementing that model, in *any* language. This has been > used historically for checking protocols for correctness, where the > specification were written in some high-level language (Haskell, Erlang) > but the code being tested were run in a low-level language (C, typically). > > In short, no single method applies in every case. Figuring out if two > programs are observationally equivalent usually requires one to exploit the > structure of the program text. Because from that structure the proof or > search strategy can be extracted. > > > -- > > You received this message because you are subscribed to the Google Groups > "golang-nuts" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to golang-nuts+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "golang-nuts" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to golang-nuts+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
