Functional Co-Programming
Aka, Functional Programming Co-Working/Learning. Everyone is welcome! We get together to learn, work, hack, connect, share, discuss…
How Are Programs Found? - by Johannes
Functional languages with strong static type systems have beneficial properties to help ensure program correctness and reliability. Surprisingly, their practical significance in applications is low relative to other languages lacking in those dimensions. In this paper, the programs-as-proofs analogy is taken seriously to gain speculative insights by analysis of creation habits in the proof-centric discipline of mathematics. Viewed in light of this analogy, a sampling of mathematicians' attitudes towards formal proof suggests that the crucial role of intuition and experimentation in programming tasks may be under appreciated, hinting at a possible explanation of the challenges rigorously disciplined languages face in practical applications.
The talk is concerned with the puzzlement over the "perennial popularity" of dynamically-typed programming languages in light of both the practical and theoretical attractiveness of statically-typed languages. We find food for thought in four episodes of 20th century and modern day mathematics, from which we try to learn about the role of functional and statically typed languages by a very generous application of Curry-Howard.
