05:20 <tankf33der> Chess engine ok as was before.

05:20 <Regenaxer> Thanks, very good

05:21 <Regenaxer> Chess changes closed then

12:38 <beneroth> Regenaxer, cess11, independently of our discussion with kluk I stumpled over this paper "Social Processes and Proofs of Theorems and Programs" from 1979 (so over 50 years old)

12:38 <beneroth> https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf

12:39 <beneroth> it's a funny read =) a bit boring in the sense that it argues the same points we do (practicability/real programming vs. program verification), a bit interesting as it is from 1979

12:40 <beneroth> Category Theory is not namely addressed in this paper, was probably also less known back then, but I don't see how the same arguments shouldn't apply in principle, too

12:42 <beneroth> the core of the argument is basically 1) mathematical proofs are social in nature, software verification methods must be too to be actually useful 2) most problems in real-world programming are not verifiable

12:43 <beneroth> it has some nice sentences in it

12:44 <beneroth> "he colorful jargon of the practicing programmer seems to be saying something about the nature of the structures he works with; maybe theoreticians ought to be listening to him. It has been estimated that more than half the code in any real production system consists of user interfaces and error messages - ad hoc, informal structures that are by definition unverifiable."

12:44 <beneroth> "In many applications, algorithm plays almost no role, and certainly presents almost no problem."

13:02 <cess11> yeah, a seasoned programmer worries more about data structures and how to make the system easy to use and available

13:03 <cess11> there are applications for formal verification, but they're pretty rare, like certain cryptographic guarantees

13:06 <cess11> personally i don't find category theory as it is commonly expressed and taught particularly intuitive, and the claim that it's based on high school algebra is treacherous

13:08 <cess11> pretty much all math stems from small sets of axioms that are partly described and applied in school so one could make the same claim for quaternionic matrix operations and strange attractors or whatever

13:11 <cess11> https://www.cognitect.com/squarespace_images/s/fsm6.png

13:11 <cess11> from https://www.cognitect.com/blog/2017/8/14/restate-your-ui-creating-a-user-interface-with-re-frame-and-state-machines

13:12 <cess11> a rudimentary state transition diagram over a login form, quite telling about where most of the work is sunk when developing applications rather than theorising models and algorithms for rather academic purposes

13:48 <beneroth> yes, I fully agree with all your statements.

15:00 <Regenaxer> beneroth, yes indeed, verification is social in nature, and most programming problems are not verifiable

15:05 <beneroth> T

15:08 <Regenaxer> Verification is a permanently ongoing process

15:10 <beneroth> hahaha, oh yes! another very important point, oft forgotten

15:11 <Regenaxer> "last bug" :)