So AI can write proofs now... how do I feel?
So first, how did I get here, into this field?
Ever since I started doing functional programming, I felt that I was on the path to building a stronger foundational understanding of Mathematics. At the time I was in university, and learning programming languages was all the rage.
I had a simple Windows HP laptop and would mainly write the simplest C programs using the Code::Blocks IDE. It felt like magic! But there was always something missing. I needed to graduate from simple Windows Console APIs and CLI programs to something practical. This would lead me to Java programming, which would land me my first tiny job: delivering an Android app for another engineering student.
As a bona fide "Android developer" at this point, I became interested in how popular apps like WhatsApp were implemented. Android development wasn't too mystical to me anymore, so I looked further, and this is how I found out about Erlang, the language behind WhatsApp's backend. And thus began my journey into functional programming.
Eve from Adam's rib??
So the LORD God caused the man to fall into a deep sleep; and while he slept, he took one of the man’s ribs and then closed up the place with flesh. And from the rib the LORD God had taken out of the man, he made a woman and brought her to him. — Genesis 2:21–22
Functional programming rewrote my entire understanding of programming. When I started learning about it, internally making copies of data structures and relying on recursion was not just counterintuitive but also seemed very slow. Somehow, functional programmers have made it work, and it has created a simpler... more "mathematical" way of reasoning about programs. Erlang takes it to the next level: if your program enters a bad state, you can "crash and recover" as fast as possible into a proper state, making the whole VM behave like a functional program! Even so, my mathematical background at the time was limited, and I failed to see how functional programming connected to what I understood of Mathematics, which to me was just a cacophony of formulas at the time. I could see how a formula is a function, but why did I need functional programming if I could write the same formula as a function in imperative C?
As I would later learn, functional programming grew out of maths the way Eve came from Adam's rib!
Theoretical Computer Science is becoming practical
The proof is left as an exercise to the reader :-D
While working on my "semi-pure" functional graph library fungi in OCaml, I have been exposed to more theoretical subjects in Computer Science that I was completely unaware of. So far I have run into three very interesting topics in Theoretical Computer Science that I have been able to build upon with my previous FP knowledge (they may be related):
- Automata Theory
- Decidability
- Curry-Howard Correspondence
Automata theory has opened up a world of understanding languages that I had completely missed in my CS undergrad. After building my interpreter-cum-compiler Craft, based on the popular book Crafting Interpreters, I am now able to revisit the project with a completely different perspective, knowing about deterministic and non-deterministic finite automata in the context of lexer and parser implementation. I am looking much deeper into proving properties about languages and using tools like the pumping lemma.
Decidability introduced me to automated theorem provers and proof checkers. As I am currently learning to use the Rocq theorem prover, I am beginning to get an idea of how some tactics like lia actually work. Decidability, correctness and proving things like termination can be very critical for some systems. Proof search may not terminate, but an interactive proof checker probably shouldn't hang. Also, since decidability is closely related to logic, we can use ideas from logic to prove things about languages, e.g. Separation Logic for proving properties of imperative languages, Hoare logic, Horn clauses, relational logic in miniKanren, etc. It's all stuff I'm piecing together.
The Curry-Howard correspondence probably put all the functional work I had done into perspective: there is a direct relationship between proofs and these programs. This gets more interesting as I use proof checkers like Rocq, which let me write total functions in a functional dialect similar to the OCaml I am familiar with. So I can technically encode my graph library in Rocq and prove some properties about it, right? .... Hmm, let me learn more about Rocq and see how far I can get :-)
Artificial Intelligence and knowledge gaps
I'll admit, I was never exposed to any of these topics before my work experience, even as an undergrad studying CS. Having leaned more towards practical programming topics during my studies, functional programming has been the only thread that has opened up these topics to me.
Anthropic recently released a blog post where they used formal verification to verify software. While there is some debate about the modelling, they have demonstrated that formal methods, which previously lived in the world of theory and weren't practical for most applications, are now feasible. This new frontier presents a different outlook on how software is delivered. Recent CVE data shows a sharp increase in exploits. Perhaps software will have to show guarantees instead of following the old worse is better approach.
As for me, this is all about the journey back to a handwritten, human understanding of proofs. I want to build a model of understanding not just software from a mathematical perspective, but also how the old mathematicians came up with their proofs. AI has been a perfect steward on this journey: I am able to build study plans around topics where the experts are completely out of reach for me. This is my journey to the source. This is how I close my knowledge gaps!
Overall, I'm excited about the future and fully welcome AI helping me understand the world better! And that's my perspective... I guess. More to come later.
← back to home