I can see "no progress in 50 years" in fundamental physics where the experimental frontier seems to be running away from us (though recent gamma astronomy results suggest a next generation accelerator really could see the dark matter particle)
In biology or chemistry it's absurd to say that -- look at metal organic frameworks or all kinds of new synthetic chemistry or ionic liquids or metagenomics, RNA structure prediction, and unraveling of how gene regulation works in the "dark genome".
Progress in the 'symbolic AI' field that includes proof assistants is a really interesting story. When I was a kid I saw an ad for Feigenbaum's 3-volume "Handbook of AI" and got a used copy years later -- you would have thought production rules (e.g. "expert systems" or "business rules") were on track to be a dominant paradigm but my understanding was that people were losing interest even before RETE engines became mainstream and even the expert system shells of the early 1980s didn't use the kind of indexing structures that are mainstream today so that whereas people we saying 10,000 rule rule bases were unruly in the 1980s, 10,000,000 well-structured rules are no problem now. Some of it is hardware but a lot of it is improvements in software.
SAT/SMT solvers (e.g. part of proof assistants) have shown steady progress in the last 50 years, though not as much as neural networks because they are less parallelization. There is dramatically more industrial use of provers though business rules engines, complex event processing, and related technologies are still marginal in the industry for reasons I don't completely understand.
>But it’s fair to assume that such fields have not been idle either.
"Manngell amnesia", where if you hear of breakthroughs in any field other than AI, you assume that very field has always been stagnant?
There's another angle to this. Eg MoF-synthesis is a breakthrough unappreciated outside of chem because of how embarrassingly easy it is. Laymen (& VCs) expect breakthroughs to require complexity, billions, wasted careers, risk, unending slog etc..
Read the bios of the chem nobellists to see what stress-free lives they led (around the time of the discovery), even compared to VCs and proof assistant researchers. Disclaimer: possibly not applicable to physics/physiology laureates after 1970 :)
Mullis succeeded in demonstrating PCR on December 16, 1983, but the staff remained circumspect as he continued to produce ambiguous results amid alleged methodological problems, including a perceived lack of "appropriate controls and repetition."
When I was a kid I saw an ad for Feigenbaum's 3-volume "Handbook of AI" and got a used copy years later
There was a Volume IV added as well at some point[1]. I've had this entire set sitting on my shelf for ages now, intending to read the entire thing "one of these days" but somehow "one day" keeps not showing up. Still, if I live long enough, I still want to read it all eventually.
Hell maybe I'll pull Volume 1 off the shelf later tonight and read a few pages, just to put a stake in the ground and say I started it at least. :-)
I'd like to call out the work from Nada Amin in this area:
Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics). Dafny Sketcher (https://github.com/namin/dafny-sketcher)
Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis.
multi-stage miniKanren (https://github.com/namin/staged-miniKanren)
> In 1994, came the Pentium with its FDIV bug: a probably insignificant but detectable error in floating-point division. The subsequent product recall cost Intel nearly half a billion dollars. John Harrison, a student of Mike’s, decided to devote his PhD research to the verification of floating-point arithmetic.
No mention of the effort by Boyer and Moore, then at their Computational Logic, Inc., to do a formal verification of the AMD FPU for the AMD5K86TM. The AMD chip shipped with no FDIV bug. [1]
ACL2 doesn't get a lot of love from the side of the verification community that focuses on the proof systems that are more academically popular (HOL family, CIC family, etc.). A lot of interesting industrial work has been done with ACL2 and related systems.
Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.
And now, Matthew Scherf has published "A Formal Specification of Advaita Vedānta in Classical High-Order Logic," and verified it in both Isabelle and Lean4. https://github.com/matthew-scherf/Advaita
In biology or chemistry it's absurd to say that -- look at metal organic frameworks or all kinds of new synthetic chemistry or ionic liquids or metagenomics, RNA structure prediction, and unraveling of how gene regulation works in the "dark genome".
Progress in the 'symbolic AI' field that includes proof assistants is a really interesting story. When I was a kid I saw an ad for Feigenbaum's 3-volume "Handbook of AI" and got a used copy years later -- you would have thought production rules (e.g. "expert systems" or "business rules") were on track to be a dominant paradigm but my understanding was that people were losing interest even before RETE engines became mainstream and even the expert system shells of the early 1980s didn't use the kind of indexing structures that are mainstream today so that whereas people we saying 10,000 rule rule bases were unruly in the 1980s, 10,000,000 well-structured rules are no problem now. Some of it is hardware but a lot of it is improvements in software.
SAT/SMT solvers (e.g. part of proof assistants) have shown steady progress in the last 50 years, though not as much as neural networks because they are less parallelization. There is dramatically more industrial use of provers though business rules engines, complex event processing, and related technologies are still marginal in the industry for reasons I don't completely understand.
>But it’s fair to assume that such fields have not been idle either.
"Manngell amnesia", where if you hear of breakthroughs in any field other than AI, you assume that very field has always been stagnant?
There's another angle to this. Eg MoF-synthesis is a breakthrough unappreciated outside of chem because of how embarrassingly easy it is. Laymen (& VCs) expect breakthroughs to require complexity, billions, wasted careers, risk, unending slog etc..
Read the bios of the chem nobellists to see what stress-free lives they led (around the time of the discovery), even compared to VCs and proof assistant researchers. Disclaimer: possibly not applicable to physics/physiology laureates after 1970 :)
https://www.amazon.com/Dancing-Naked-Mind-Field-Mullis/dp/07...
Mullis succeeded in demonstrating PCR on December 16, 1983, but the staff remained circumspect as he continued to produce ambiguous results amid alleged methodological problems, including a perceived lack of "appropriate controls and repetition."
(From wiki)
There was a Volume IV added as well at some point[1]. I've had this entire set sitting on my shelf for ages now, intending to read the entire thing "one of these days" but somehow "one day" keeps not showing up. Still, if I live long enough, I still want to read it all eventually.
Hell maybe I'll pull Volume 1 off the shelf later tonight and read a few pages, just to put a stake in the ground and say I started it at least. :-)
[1]: https://www.amazon.com/Handbook-Artificial-Intelligence-IV/d...
Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics). Dafny Sketcher (https://github.com/namin/dafny-sketcher)
Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis. multi-stage miniKanren (https://github.com/namin/staged-miniKanren)
Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems. VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-...), and Holey (https://github.com/namin/holey).
Nada Amin website - https://namin.seas.harvard.edu/
No mention of the effort by Boyer and Moore, then at their Computational Logic, Inc., to do a formal verification of the AMD FPU for the AMD5K86TM. The AMD chip shipped with no FDIV bug. [1]
[1] https://dl.acm.org/doi/abs/10.1109/12.713311