Linear logic has been known since 1987. The first release of Coq (dependent types for functional programming and writing proofs) was in 1989. The HoTTBook came out in 2013. Ada/SPARK 2014 came out the same year as Java 8 did. We also witnessed the Software Foundations series, the CompCert C compiler, the Sel4 microkernel, and the SPARKNaCl cryptographic library. Instead of learning about those achievements and aiming to program for the same reliability, clarity, and sophistication, we see an abundance of software that cannot clearly describe their own behavior nor misbehavior. Instead of incorporating the full functionality of XML/HTML/CSS/SVG/JS/WebGL into the development experience and providing ways to control them at the fundamental level, we reinvent crude approximations like the various web frameworks. YAML and JSON often trumps XML/XSD until things get out of control, and even then, people still don’t learn the lesson. Protobuf, flatbuffer, capnproto, and the like keep reinventing ASN.1. Naive microservices partially reimplements Erlang’s BEAM VM while ignoring all the hard parts that BEAM VM got right. Many people riding the microservice bandwagon have never even heard of Paxos, not to mention TLA+. Many programmers keep learning new shining frameworks but are reluctant to learn about the crucial fundamentals, e.g., Introduction to Parallel Algorithms and Architectures, nor how to think clearly and unambiguously in the spirit of Coq/Agda/Lean. No wonder ChatGPT exposes how shallow most of programming is and how lacking most programmers are in actual understanding. Linear logic and dependent types are there to help us design and think with clarity at a high level, but people would rather fumble around with OOP class hierarchies (participate in the pointless is-a/has-a arguments) and “architecture” design that only complicate things. What is this madness? This doesn’t sound like engineering.
Story Published at: February 10, 2023 at 08:28AM
Story Published at: February 10, 2023 at 08:28AM