jtojnar has quit [Remote host closed the connection]
Lisanna has joined #nixos-chat
ashgillman has quit [Ping timeout: 240 seconds]
<shlevy>
MichaelRaskin: QED manifesto was... bold :D "Based upon discussions with numerous workers in automated reasoning, it is our view that using current proof-checking technology, we can, using a variety of systems and expert users of those systems, check mathematics at within a factor of ten, often much better, of the time it takes a skilled mathematician to write down a proof at the level of an advanced undergraduate textbook. "
<shlevy>
Has proof-checking technology fallen so far in 24 years? :D
<MichaelRaskin>
shlevy: proof-checking technology is not what you want to look at.
<MichaelRaskin>
The most powerful technology — both then and now — is for automated proof generation in ATP.
<MichaelRaskin>
Of course, for FO:
<MichaelRaskin>
FIL
<MichaelRaskin>
FOL
<MichaelRaskin>
(I meant FOL and I cannot type correctly)
<MichaelRaskin>
We have a kind of uncontrollable excavator — FOL provers, but everyone is busy polishing the spades like Coq.
jtojnar has joined #nixos-chat
<MichaelRaskin>
shlevy: also, have you ever published a purely theoretical paper? Because I have a feeling they meant writing down a proof that has never been written at the advanced-undergraduate level, and writing it at this later takes more time than you would expect.
<MichaelRaskin>
As for technology regress (or lack of progress) — watch The Demo, read the Engelbart's report corresponding to the demo and tell me what has happenned to information processing systems in the last 50 years. It's not lack of progress, it's just progress in a completely different direction
<MichaelRaskin>
(Yes, the actual direction is worse in many aspects)
ashgillman has joined #nixos-chat
Synthetica has joined #nixos-chat
ashgillman has quit [Ping timeout: 240 seconds]
<shlevy>
MichaelRaskin: Ah, if they're talking about writing novel work, that's a bit more understandable
<shlevy>
MichaelRaskin: I thought there were serious projects based around FOL and complete automation though?
<MichaelRaskin>
shlevy: I think they are comparing to writing new textbooks on the material that exists only in the articles.
<shlevy>
I see
<MichaelRaskin>
Well, I guess writing a new book on an old topic without any access to old textbooks would also ocunt
<MichaelRaskin>
count
<MichaelRaskin>
As far as I know, the first-order situation is complicated
<MichaelRaskin>
There is a lot of good work on first-order provers
<MichaelRaskin>
But this is work on things that can be proven from axioms to full proof fully automatically.
<shlevy>
What would you want to see instead?
<MichaelRaskin>
Not instead — in addition
<MichaelRaskin>
Something that I have even tried to do and will try again at some point, but I would like to see more of that…
<MichaelRaskin>
Basically, there is TPTP
<MichaelRaskin>
A collection of test problems for ATP (mostly FOL ATP)
<MichaelRaskin>
When I tried to experiment with guided proofs (I give lemmas, I want formal proof), I found that: 1) formal grammar for TPTP language was slightly wrong — promptly fixed after a bugreport, and 2) set theory axioms — which are hard to use in a fully-automated setting — contain some silly typos (also fixed)
<MichaelRaskin>
And of course for set theory representation matters, and I have the feeling that the available axiom sets have been selected by theoretically considering the idea of ATP
<shlevy>
So in your view of a guided proof, you *prove* a lemma, or you state a lemma that the prover proves first and then uses in the broader proof?
<MichaelRaskin>
I would love to see more guided proof work, and some axiom sets that look like they are compatible with guided proofs.
<MichaelRaskin>
shlevy: well, in the ideal world I would formalise the lemma statements from a paper, see which steps cna be filled completely. Find those two hard lemmas, formalise every step as written for humans, make the ATP fill formalities. Find that one hard step, and give it formalism-level intermediate steps to prove.
<shlevy>
Gotcha
<shlevy>
And you think most (all?) interesting work can be done with FOL + non-controversial (to normal mathematicians at least) axiom sets?
<MichaelRaskin>
Note that this dream is inherently parallelism-friendly — unrelated lemmas can be processed in parallel, and if I am sure some lemma is true, the steps before it and the steps based on it can also run in parallel
<shlevy>
Or do you have a view on what the process should look like when you need to reach beyond FOL? Maybe the same, just you might have to do more guidance?
<MichaelRaskin>
I do not think that the requirement of an axiom set to be uncontroversial is that useful.
<shlevy>
How about the requirement that the union of axiom sets be relatively straightforward to grasp by a human reviewing your work?
<MichaelRaskin>
I think that things beyond FOL can be immersed as a carefully-constructed axiom set for FOL.
<MichaelRaskin>
shlevy: how about the current requirement that you need to find a venue where your set of definitions is recognised to make sense?
<shlevy>
The thing I like about small systems is the hope that you can look at the spec and understand the base system without knowing anything about the specific proof, and have a sense of what is really being said. I worry freely throwing in axioms, however justified, might undermine that.
<shlevy>
I don't quite understand what you mean, sorry
<MichaelRaskin>
Right now some subfields of maths study the objects that only make sense if you make a decision on Continuum Hypothesis, and these subfields of maths do not normally talk in terms of CH.
<shlevy>
OK...
<MichaelRaskin>
If you want to verify a program specification that doesn't rely on probability at all, you have a good chance to limit everything to a widely-recognised encoding of PA. Or a weaker arithmetics + some finite-structure theory.
<MichaelRaskin>
If you want to rely on the central limit theorem, well, it is heavy, but maybe formal verification will give a boost to reverse mathematics around it.
<shlevy>
Sure. I guess my concern is about building a system that works for 80% of cases very well but doesn't have a viable escape hatch for the hard 20% (or even 95%/5%).
<MichaelRaskin>
If you can convince humans, you are effectively talking in FOL + axioms
<shlevy>
The escape hatch doesn't have to be pretty, but if it causes people to leave the system altogether (or leave verification altogether, heaven forbid ;) ) then IMO it undermines the overall project.
<shlevy>
OK
<MichaelRaskin>
Maybe your axioms are «whatever is proven in CoC can be trusted» — yes, you can encode this using a FOL computation model
<shlevy>
Do you have any references expanding on that point (or related points) in detail? I'd be curious to see what the full argument looks like
<MichaelRaskin>
About what?
<shlevy>
That FOL + axioms should be enough
<MichaelRaskin>
I want to say «Aristotle»
<shlevy>
:D
<MichaelRaskin>
I mean, whatever type theorists say, the only realistic logic step you can use to convince physicists is modus ponens.
<shlevy>
At first guess (not based on any heavy experience) I'd say I'd usually want to reach for HOL when proving metatheorems as code reuse
<shlevy>
But I don't actually mind having those not be proven themselves and merely proving the outputs
<shlevy>
So long as that doesn't result in significant inefficiency in having to actually *run* the HOL step in every proof
<MichaelRaskin>
Well, maybe its my staring into abyss talking, but when you say HOL I want to ask «could we please just follow Henkin?»
<shlevy>
Meaning?
<MichaelRaskin>
I am almost sure that Henkin semantics would satisfy all your _real_ goals behind wanting HOL, and at the same time it is basically FOL and can be modelled in FOL.
<shlevy>
Ah OK
<shlevy>
So what is your most charitable explanation for why so many seem to reach for other HOLs? :)
<MichaelRaskin>
Henkin semantics means that you introduce higher-order objects and some operations on them and some properties of them, then say that subsets is whatever satisfies the requirements on subsets
<MichaelRaskin>
You are prohibited from doing this trick from HOL «obviously I require _all_ subsets»
<MichaelRaskin>
Well, there is this nice claim that second-order Peano arithmetics uniquely specified integers.
<MichaelRaskin>
People take it at face value.
<sorear>
first order logic has all of the functions and predicates you want, they just exist in the universe. HOL studies the integers with a complicated logic, FOL studies deeply nested & infinite sets with a simple logic, it's a reshuffling of complexity not a difference in power
<MichaelRaskin>
(Cthulhu laughs behind the scene)
obadz has quit [Ping timeout: 260 seconds]
<MichaelRaskin>
sorear: HOL slightly hides the real requirements on the set theory.
obadz has joined #nixos-chat
<MichaelRaskin>
FOL can be used on a very weak arithmetics with a separate finite-sequence object type (recursive or not)
<MichaelRaskin>
FOL doesn't allow to abstract away completely any part of the theory of structures — which is both a benefit and a drawback.
<sphalerite>
<and now for something completely different!>
<sphalerite>
will 64-bit word size stop being enough for general-purpose computing within the foreseeable future?
<sorear>
i suppose that depends on how you define "general purpose"
<sorear>
32-bit machines are still with us and will be for quite a while
<MichaelRaskin>
Yes, because the advances in fast non-volatile RAM will mimick the storage technology and accidentally import ≥1KiB pages.
<MichaelRaskin>
No, because a reprapish kind of distributed fabrication will make 16-bit controllers a desirable target, so some people will make sure they can do as much as possible there.
<MichaelRaskin>
No, because word size will lose its meaning for a complicated enough cache hierarchy.
<MichaelRaskin>
No, because general-purpose computing will be stamped out by Apple.
<sphalerite>
ha
<sphalerite>
last I heard their products were on a bit of a downward slope
<MichaelRaskin>
They have a lot of cash and generl-purpose computing is a problem for their business model
<sorear>
you and I have different definitions of "general-purpose computing" then
<MichaelRaskin>
I think their products are on a downward slope since iPhone, it just takes time to become obvious.
<sorear>
there is nothing in my definition of "general-purpose computing" that *requires* permissionlessness
<MichaelRaskin>
(I mean, after seeing iPhone as a physical object, I lost a significant amount of respect)
<sorear>
an iphone is not *your* general-purpose computer, but it is one
<MichaelRaskin>
iPhone is definitely a general-purpose computer
<MichaelRaskin>
Apple would be completely happy, though, to sell appliances that do only what people Actually Need.
<MichaelRaskin>
Which doesn't include any actual information processing, if they can have their way.
<sorear>
so you think they're going to voluntarily walk away from the giant free money machine that is the app store?
<MichaelRaskin>
sorear: I hope they just won't get a chance; but if they do, 75% of the appstore revenue would come from in-game purchases in games that differ only in reskinning
<MichaelRaskin>
And even if a tower defense level editor allows creating a level modelling a Turing machine, it is not really general-purpose computation in my opinion.
<MichaelRaskin>
(Also: modern HDDs seem to have faster CPUs and more RAM than the computer I used when learning to program, I still don't think of HDDs as general purpose computation devices on their own)
Synthetica has quit [Quit: Connection closed for inactivity]
Lisanna has quit [Quit: Lisanna]
joepie91___ has joined #nixos-chat
joepie91 has quit [Excess Flood]
boomshroom has joined #nixos-chat
<boomshroom>
I often spend time in the main nixos channel. I figure I may as well check out this channel. Seems less active though.
<MichaelRaskin>
This channel is relatively new
<MichaelRaskin>
And I would say it's bursty.
<sphalerite>
lots of MichaelRaskin talking about scary complicated-sounding things :D
<MichaelRaskin>
I'm not even always here!
<andi->
What are you guys using (mostly tools, not so much physical entity) to run one-off (nix(os)) builds on some $infrastructure provider for a few bucks/hour? I am currently in need of more computation power but do not want to manually have to deal with all the hazzle of configuring servers... I could probably use NixOPS for that and write a few custom expressions..
<boomshroom>
andi-: My custom gaming rig. :P
<andi->
boomshroom: yes, but I mean proper hardware >20 cores amd64 ;)
joepie91___ is now known as joepie91
boomshroom is now known as boomshroom-away
infinisil has quit [Quit: Configuring ZNC, sorry for the join/quits!]
infinisil has joined #nixos-chat
infinisil has quit [Quit: Configuring ZNC, sorry for the join/quits!]
infinisil has joined #nixos-chat
infinisil has quit [Quit: Configuring ZNC, sorry for the join/quits!]
infinisil has joined #nixos-chat
infinisil has quit [Quit: Configuring ZNC, sorry for the join/quits!]