Oh I just noticed, @Apostolis it was from your post that I learned about Tangible Functional Programming. Thanks for that, I like the concept and since then have been studying the author’s work, following the path of research. I resonate with the line of thinking and subjects he’s engaged in, for example:
Why might one care about interpreting lambda expressions in terms of cartesian closed categories (CCCs)..? I got interested because I’ve been thinking about how to compile Haskell programs to “circuits”, both the standard static kind and more dynamic variants. Since Haskell is a typed lambda calculus, if we can formulate circuits as a CCC, we’ll have our Haskell-to-circuit compiler.
– Circuits as a bicartesian closed category and From Haskell to hardware via cartesian closed categories
My hunch is that combinatory logic and linear logic are relevant to this question.
Maybe a network can be considered a large-scale circuit with asynchronous signals and processes. I imagine software design can learn more from how existing hardware systems solve the question of entropy, uncertainty, unreliability - building a (more) deterministic and predictable system with strategies like fault tolerance, error correction, exception handling.
Here’s a recent talk by the same author.
It’s about how the current practice of programming and software development has created a big mess, and how formal logic, correctness, proofs, and mathematics can provide the solid foundation for a better approach.
Haskell, Rust, Lean.. From these I’m fond of Haskell, and slowly learning to read Rust because it’s practical and popular. I’m curious about Rocq and Agda too, since some of the researchers I’m interested in are using them to communicate their ideas.
In Galileo’s time, professors of philosophy and theology—the subjects were inseparable—produced grand discourses on the nature of reality, the structure of the universe, and the way the world works, all based on sophisticated metaphysical arguments.
Meanwhile, Galileo measured how fast balls roll down inclined planes. How mundane! But the learned discourses, while grand, were vague. Galileo’s investigations were clear and precise. The old metaphysics never progressed, while Galileo’s work bore abundant, and at length spectacular, fruit. Galileo too cared about the big questions, but he realized that getting genuine answers requires patience and humility before the facts.
– Frank Wilczek, The Lightness of Being: Mass, Ether, and the Unification of Forces