It highly depends on what you define a function. If it's in the mathematical sense, it won't work.
A function, in practice, is a small embedded program (stored as a valur in the main program). It's not just the text (semantics). It's defined somewhere (in some package etc...) That's all those things that probably need to be equal. On Friday, November 25, 2016 at 12:28:52 PM UTC+1, Jesper Louis Andersen wrote: > > 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 < > golan...@googlegroups.com <javascript:>> 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.lou...@gmail.com <javascript:>> wrote: >> >>> >>> On Fri, Nov 25, 2016 at 12:30 AM Michael Jones <michae...@gmail.com >>> <javascript:>> 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...@googlegroups.com <javascript:>. >>> 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...@googlegroups.com <javascript:>. >> 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.
