_______ __ _______
| | |.---.-..----.| |--..-----..----. | | |.-----..--.--.--..-----.
| || _ || __|| < | -__|| _| | || -__|| | | ||__ --|
|___|___||___._||____||__|__||_____||__| |__|____||_____||________||_____|
on Gopher (inofficial)
(HTM) Visit Hacker News on the Web
COMMENT PAGE FOR:
(HTM) 50 years of proof assistants
Agingcoder wrote 18 hours 50 min ago:
Very nice post thanks - I didnât know about cakeml and bootstrapping
formally verified compilers.
hamiecod wrote 1 day ago:
I recently started reading "Specifying Systems: The TLA+ Language and
Tools for Hardware and Software En" by Lawrence Lamport[0]. It is a
good starting point for learning how to specify systems on the basis of
mathematical proofs.
Since the new code is specifications in the age of AI, learning how to
specify systems mathematically is a huge advantage because English is
extremely ambiguous.
[0]:
(HTM) [1]: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
gmfawcett wrote 20 hours 56 min ago:
I've had the same intuition. I've had mixed results in this area,
although I'm certainly no expert. Recently I wanted to formalize a
model of a runbook for a tricky system migration, to help me reason
through some alternatives. I ended up writing a TLA+ spec before
generating some visualizations, and also some possible prototypes in
MiniZinc. All three (spec, visualizations, CP models) were vibe-coded
in different sessions, in about that order, though most of my
personal effort went into the spec.
While the later AIs quickly understood many aspects of the spec, they
struggled with certain constraints whose intuitive meaning was
concealed behind too much math. Matters which I had assumed were
completely settled, because a precise constraint existed in the spec,
had to be re-explained to the AI after implementation errors were
found. Eventually, I added more spec comments to explain the
motivation for some of the constraints, which helped somewhat. (While
it's an untested idea, my next step was going to be to capture traces
of the TLA+ spec being tested against some toy models, and including
those traces as inputs when producing the implementations, e.g. to
construct unit tests. Reasoning about traces seemed to be a fairly
strong suit for the AI helper.)
In hindsight, I feel I set my sights a little too high. A human
reader would have had similar comprehension problems with my spec,
and they probably would have taken longer to prime themselves than
the AI did. Perhaps my takeaway is that TLA+ is a great way to model
certain systems mathematically, because precision in meaning is a
great quality; but you still have to show sympathy to your reader.
mnky9800n wrote 1 day ago:
I think when Peter Thiel talks about stagnation itâs as much about
the vibe of things as it is quantifying metrics of progress. I happen
to agree with the idea that the vibe of progress has unilaterally
focused on ai and computer technology even though this isnât the case
for metrics (e.g., CRISPR). I think the stagnation vibe has come from a
series of issues such as decades of American political gridlock,
Europes inability to commit to anything, the rise of the attention
economy, the stagnation of Japan, the lack of a competitive focus for
American markets (with no Soviet Union to defeat they seemed to have
turned to defeating billionaire poverty). This list continues but
itâs the confluence of all these things that gives the vibe of
stagnation. It seems like there isnât enough time to focus on
anything anymore to actually get excited to drive it forward. Even
though this isnât the case. And there also isnât the political
space to celebrate things. Like it seems like any spacex accomplishment
should be followed with the caveat that you donât like Elon. Another
way I think about this is that we live in this post cynicism world
where we all have to couch every statement within some framework
acknowledging harm to someone somehow. Itâs hard to have a vibe of
progress when every statement of progress includes an impact statement
saying why that progress is harmful.
polskibus wrote 1 day ago:
Lean4 seems to be very popular in the Math Olympics-solving AI startups
(Harmonic etc).
seanhunter wrote 1 day ago:
â¦and is now being taught in combined âFormal Real Analysisâ[1]
courses to undergrads, and the lean prover community has a joint
project to formalize the proof of Fermatâs Last Theorem, which is a
lot of work but is progressing. Itâs sort of weird to say there is
no progress. It seems to me when you have a fields medal winner
publishing lean4 formal proofs on github[2] to go with one of his
books you are making a lot of progress. [1] eg [1]
(HTM) [1]: https://youtube.com/playlist?list=PLs6rMe3K87LHu03WWh9rEbEhh...
(HTM) [2]: https://github.com/teorth/analysis
adyashakti wrote 1 day ago:
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.
(HTM) [1]: https://github.com/matthew-scherf/Advaita
hamiecod wrote 1 day ago:
This is funny as well as amazing haha. This makes me wonder whether
mathematics can prove the real truth or not since it does not take
spirituality, conciousness and metaphysics (things we dont yet fully
understand) into account.
juliangamble wrote 1 day ago:
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 ( [1] )
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 ( [2] )
Monte Carlo Tree Search, specifically the VerMCTS variant, and when
this exploration-exploitation sweet spot is a good match for synthesis
problems.
VerMCTS ( [3] ), and Holey ( [4] ).
(HTM) [1]: https://github.com/namin/dafny-sketcher
(HTM) [2]: https://github.com/namin/staged-miniKanren
(HTM) [3]: https://github.com/namin/llm-verified-with-monte-carlo-tree-se...
(HTM) [4]: https://github.com/namin/holey
mccoyb wrote 12 hours 39 min ago:
Nada is the best! Don't forget the mind bending [1] (not quite on
topic, but in the multi-stage rabbit hole)
(HTM) [1]: https://dl.acm.org/doi/10.1145/3158140
rramadass wrote 1 day ago:
Very Interesting; thanks for the pointer.
Nada Amin website -
(HTM) [1]: https://namin.seas.harvard.edu/
PaulHoule wrote 1 day ago:
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.
didericis wrote 1 day ago:
> business rules engines, complex event processing, and related
technologies are still marginal in the industry for reasons I don't
completely understand
Translating between complex implicit intention in colloquial language
and software and formal language used in proof assistants is usually
very time consuming and difficult.
By the time youâve formalized the rules, the context in which the
rules made sense will have changed/a lot will be outdated. Plus time
and money spent on formalizing rules is time and money not spent on
core business needs.
PaulHoule wrote 19 hours 49 min ago:
That's definitely true, but I do think production rules have some
uses that are less obvious.
For instance, XSLT is not "an overcomplicated Jinja 2" but rather
it is based on production rules but hardly anybody seems to know
that, they just think it's a Jinja 2 that doesn't do what they
want.
Production rules are remarkably effective at dealing with deep
asynchrony, say a process that involves some steps done by people
or some steps done by humans, like a loan application being
processed by a bank that has to be looked at by a loan officer.
They could be an answer to the async comm problems in the web
browser. See also complex events processing.
Production rules could be a more disciplined way to address the
issues addressed by stored procedures in databases.
I've written systems where production rules are used in the control
plane to set up and tear down data pipelines with multiple phases
in a way that can exploit the opportunistic parallelism that can be
found in sprawling commercial batch jobs. (The Jena folks told me
what I was doing wasn't supported but I'd spent a lot of time with
the source code and there was no problem.)
gsf_emergency_6 wrote 1 day ago:
>in biology or chemistry..
>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 :) [1] 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)
(HTM) [1]: https://www.amazon.com/Dancing-Naked-Mind-Field-Mullis/dp/07...
PaulHoule wrote 1 day ago:
There was one day the bus was late so I drove in with a grad
student who did density functional theory calculations of MOFs and
asked him "How do you make a MOF?" and he said "Beats me, I'm a
theorist" so I figured that I wanted a quick answer to that one
myself and it turned out to be "mix up the ingredients and bake
them in the oven"
gsf_emergency_6 wrote 20 hours 13 min ago:
It looks like that the "theorist" might be replaced sooner, given
the narratives that are being driven now.. (after the entry level
coder)
PaulHoule wrote 18 hours 6 min ago:
I'll say grad students today often seem a bit sheepish and
inarticulate. They're facing a very competitive market so I
think it behooves the theorists to be able to talk about
experiment a bit and vice versa. On the other hand they have a
big hill to climb to just be successful with DFT.
One of my few regrets in grad school is that I didn't take a
course in DFT, not like I was really going to use it, but DFT
is an example of the kind of very complex calculation which
takes a lot of care to apply. I got a little of this art from
Sethna's class in renormalization groups and such but it was
really [1] by Chandrasekhar that taught me how to organize the
kind of complex calculations that might involve numeric
integration differential equations, using a computer, etc --
extracurricular for a cond-mat PhD but really a lot of fun.
I just made a breakthrough in selfobject technology (enough of
a reformulation that I can take back the ideas that my evil
twin published in such a way that I couldn't ever publish them
under my name) and managed to get the evil out of my evil twin
and I've been practicing "radiance drills" that get me into a
state where I can really draw out 30y+ people but how it works
with "kids these days" is an open question because since the
pandemic grad students mostly seem like damp squibs -- I gotta
give it a try.
I do regret I didn't figure this out much sooner (if I had I
wouldn't have some things on my chart I do now) but right now I
having so much fun I think other people should be jealous.
(HTM) [1]: https://www.amazon.com/Introduction-Study-Stellar-Stru...
gsf_emergency_6 wrote 14 hours 30 min ago:
Have you asked LLMs about the VASP codebase? With special
reference to Tomas Arias' flow-chart(s) [0]
Grad students these days will need to figure out their
Altman-informed version of radiance (maybe easier if they
spend more time on some dank corners of HN).
I'm jealous you found Chandrasekhar :) going to look at this
to train understanding of human and/or AI pedagogy.
I too have my favorite Dover books (Lanczos, Yaglom, the
"Green books") but I can't say I got any general techne out
of them (yet) [1] These are the underappreciated infra born
of the preAI cold-war times (doubt postsoviet mathematicians
have an equivalent. Especially not "Bourbaki" =P)!
Worth recommending to gen-A/Z so they have an inkling what
semifunctional social infra looked like before
*verflow/*stackexchange
[0] [2] Or page 95
(HTM) [1]: https://www.amazon.com/Applied-Analysis-Cornelius-La...
(HTM) [2]: https://www.linkedin.com/posts/juarezlfdasilva_flowc...
(HTM) [3]: https://dspace.mit.edu/bitstream/handle/1721.1/8282/...
mindcrime wrote 1 day ago:
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. :-)
[1]
(HTM) [1]: https://www.amazon.com/Handbook-Artificial-Intelligence-IV/d...
ebcode wrote 21 hours 41 min ago:
I picked these up at a used bookstore ages ago, since they had the
three-volume set. My recommendation would be to familiarize
yourself with just the table of contents thatâs printed on the
binding, and when you come across something adjacent in your
day-to-day work (e.g. Search), review the papers in that section.
Those books are an excellent snapshot of the field at the time.
ratmice wrote 1 day ago:
I wish he had just said 50 years of LCF, since he even mentions
automath in the article but that was but that was late 60s
robinzfc wrote 1 day ago:
Yes, 50 years of LCF would have been much better. You should not talk
about "50 years of proof assistants" and not mention Mizar which had
the largest library of theorems for about half of that time.
Animats wrote 1 day ago:
> 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]
(HTM) [1]: https://dl.acm.org/doi/abs/10.1109/12.713311
porcoda wrote 1 day ago:
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.
Animats wrote 1 day ago:
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.
porcoda wrote 1 day ago:
I assume you mean first SMT solver when you refer to
Oppen-Nelson? I thought their contribution was the basis for SMT
methods.
(DIR) <- back to front page