iiinova — where your digital self keeps evolving

boarders.bsky.social @boarders.bsky.social · 25m

you win the award for the person I most expect on here to be reading a biology book by a biologist who happens to know homology and cat theory

120

boarders.bsky.social @boarders.bsky.social · 47m

I strongly dislike the semantic under-determinism of what a commit message or commit history should be -- should it be some kind of rationally re-constructed series of design decisions, or should be be a historical account of development -- and I rather resent it as a halfway house of neither

010

boarders.bsky.social @boarders.bsky.social · 51m

the current victory of connectionist/historicist methodologies over rationalist methodologies and who supports each story is really fascinating if you are a sicko

100

boarders.bsky.social @boarders.bsky.social · 52m

but I recognize people will have radically different experiences, and really can be way closer to one end or the other in the kinds of things they work on and think about

000

boarders.bsky.social @boarders.bsky.social · 52m

in software of the sort I do, there is a constant push and pull between these dynamics and some of the fun of the discipline to me is to try to figure out what is mathematics, and what parts are computational/empirical and how can I get the two to best interact

110

boarders.bsky.social @boarders.bsky.social · 54m

which involves a kludge of many different interlocking systems and insights which we use to constrain the computational world in various ways we learn how to, but which in no way comes close to a formal mathematical specification of anything

210

boarders.bsky.social @boarders.bsky.social · 54m

in my way of thinking, wherever we can get formal mathematical models of something we should cherish that as a crown jewel e.g. compcert giving a compiler which has a formal semantics of C is an incredible achievement, but we what we are doing is often closer to 'modelling the weather system'

110

boarders.bsky.social @boarders.bsky.social · 56m

I wouldn't quite say it like that, we should hold onto and cherish as much as we can about the formal thing at the heart of something, and then accept the bitter lesson of computation that we don't have a formal mathematical model of the entire scenario

110

boarders.bsky.social @boarders.bsky.social · 1h

On the other hand, one aspect of any engineering discipline is how one designs for fault/precision tolerance, and it really often misleads us to think all of our systems are anything close to formal semantics compared to something closer to empirical object with constraints

130

boarders.bsky.social @boarders.bsky.social · 1h

I agree with that, but I will say that a compiler has something at least approaching a formal mathematical theory of what correctness might mean, and I think that must be part of the consideration with how one thinks about these things

110

boarders.bsky.social @boarders.bsky.social · 1h

I remember being young and getting morphine in a hospital and my dad telling me it is chemically essentially the same as heroin and that radically re-shaping how I thought about drugs, addiction, the I'd been misled into believing about drugs creating instant and permanent chemical dependence etc.

010

boarders.bsky.social @boarders.bsky.social · 1h

she seems one of the democrats who is better able to adapt to a changing environment (not sure I would have predicted that, but it does seem to be the case)

030

boarders.bsky.social @boarders.bsky.social · 2h

how about programs that call a relational database, how about differences in arithmetic semantics, or in the under-determination of specs (IEEE floating point, json etc.), how about how they handle timing and branching (which is observable behaviour to a cryptographic program!) etc etc etc.

020

boarders.bsky.social @boarders.bsky.social · 2h

100% agree and I think it is shocking how much people don't think about how complex observational equivalence of programs really can be. Some examples include: when are these two programs that use rng the same, how about concurrency

120

boarders.bsky.social @boarders.bsky.social · 4h

it’s the cope that kills you

010

boarders.bsky.social @boarders.bsky.social · 4h

what I don't understand is I am sure one could have many uses for using it to enhance lecture notes e.g. turning markdown notes to latex, help with tikz diagrams, asking about the correct logical ordering to put certain material (perhaps) etc. but writing the actual course material? huh??

140

boarders.bsky.social @boarders.bsky.social · 4h

The above clay institute document defines in mathematical terms what ‘physically reasonable’ means and the openAI solution satisfies those purely mathematical conditions

120

boarders.bsky.social @boarders.bsky.social · 4h

and what does that document define "physically reasonable" to mean?

010

boarders.bsky.social @boarders.bsky.social · 4h

if the openAI paper (which I am sure is atrociously written) claims that, then that is not great as a piece of scientific communication, but it has no bearing on whether they solved one variant of the NS problem, which they did

030

boarders.bsky.social @boarders.bsky.social · 5h

I think about this image and the one about the banker who can say slurs against disabled people again way too often

041

boarders.bsky.social @boarders.bsky.social · 5h

It is like stating you haven't solved the poincaré conjecture because what we _really_ care about is the smooth poincaré conjecture

110

boarders.bsky.social @boarders.bsky.social · 5h

I will just say that mathematicians all the time care about these kinds of distinctions (smooth vs real analytic) and many problems are secretly regimes of different problem types, but the idea that one counts as having solved a clearly stated problem and the other doesn't is nonsense

110

boarders.bsky.social @boarders.bsky.social · 5h

I'd be happy to know any source that gave you this impression

150

boarders.bsky.social @boarders.bsky.social · 5h

I know for a fact that mathematicians as a whole don't think this or agree with you, but I want to know if what you are saying is based on anything according to you

040

boarders.bsky.social @boarders.bsky.social · 5h

can you provide a single paper or even source of any kind which backs up the claim that the millennium problems were specifically only about a physically meaningful or possible input?

270

boarders.bsky.social @boarders.bsky.social · 5h

I agree we won't do human rewrites, I just think almost all of the work of rewrites is moved towards verification, and most people will need some slightly compelling reason to want to do that sort of verification compared to the many other things they have to do

010

boarders.bsky.social @boarders.bsky.social · 5h

Ah got it, I think constantly re-writing code will be a waste of agent's time, it seems to me they are better off writing provably correct transpilers or something higher value than acting as intergalactic translators

130

boarders.bsky.social @boarders.bsky.social · 5h

if I have a large and complex codebase, then I would like various core components to be highly trustworthy with good boundaries. Until the point one has a specification for synthesizing the exact code and interfaces, I wouldn't want to just rewrite it for lack of belief that I can trust the outcome

050

boarders.bsky.social @boarders.bsky.social · 5h

I don't fully follow how that answers what I've said

110

boarders.bsky.social @boarders.bsky.social · 5h

worth saying that the lean kernel goes way beyond implementing the type theory in carneiro's thesis, so this is a different source of issues which is that people would like lean to be expressive enough for complicated constructs, but this comes into conflict with whether what is implemented is sound

010

boarders.bsky.social @boarders.bsky.social · 5h

I am sure the cost or rewrites is going to plummet, but I think this seems like a big waste of time, and based on some fallacy that if the agent does it then it comes at no cost. Surely we will have better things to do with our time (and agent's time) than constantly doing huge rewrites?

230

boarders.bsky.social @boarders.bsky.social · 5h

and actually all of the above should be ZFC + inaccessible cardianals / grothendieck universes (I wrote ZFC+ for it in the last post)

010

boarders.bsky.social @boarders.bsky.social · 5h

didn't capture all the features that the lean kernel implements. Recently the lean team wrote a new kernel in lean itself which proves that the type theory has a model in ZFC+. This is, of course, circular so only shows lean is sound if you believe the proof doesn't use some unsound feature of lean

320

boarders.bsky.social @boarders.bsky.social · 5h

It depends on the type theory, martin-löf dependent type theory (or variants like homotopy type theory/cubical type theory) have models in set theory and so are sound wrt ZFC. The type theory of lean had a proof due to Mario Carneiro that it had a model in ZFC, but the proof was incorrect, and /...

120

boarders.bsky.social @boarders.bsky.social · 7h

a related example is Quine's new foundations: en.wikipedia.org/wiki/New_Fou... which has had controversy over its soundness since it existed

en.wikipedia.org

New Foundations - Wikipedia

020

boarders.bsky.social @boarders.bsky.social · 7h

and those aspects are not well understood. It is actually very analogous to adding a new axiom to ZFC (or several) and wondering if what you get is still consistent with ZFC

110

boarders.bsky.social @boarders.bsky.social · 7h

well apologies if so, but your questions don't clarify it, why would it make a difference that ZFC doesn't have contradictions compared with an implementation of a type theory? The rules that cause the contradiction are subtle aspects of the theory (e.g. the type theory of nested inductives)

210

boarders.bsky.social @boarders.bsky.social · 7h

universes and it was incorrect. For your second point, because one can draw a contradiction from the rules of the logic, it doesn't mean it will be easy, it can be just as hard as any counter-example in mathematics

110

boarders.bsky.social @boarders.bsky.social · 7h

yes, so it may be hard to construct a formal model in ZFC set theory (e.g. can one construct a model for ZFC + CH, well yes but that is a hard theorem of Godel) for all of the rules which end up being complicated (e.g. there was an original proof that lean has a model in ZFC + grothendieck /...

110

boarders.bsky.social @boarders.bsky.social · 7h

this was exploiting a bug in the kernel (actually two different bugs in two different kernels iirc)

010

boarders.bsky.social @boarders.bsky.social · 7h

How do you imagine an ordinary proof of soundness or unsoundness of a logic looks?

120

boarders.bsky.social @boarders.bsky.social · 9h

this is why I like to write R[x,y] as R[x,x] since they are both definitionally equal

130

boarders.bsky.social @boarders.bsky.social · 9h

anthropologists: curiously, humans have been anatomically modern for around 200,000 years but are only thought to have developed what we would identify as modern behaviour around 50,000 years ago with what is thought to be the emergence of language. I wonder why it took so long?

010

boarders.bsky.social @boarders.bsky.social · 9h

important in itself. But it it perfectly plausible to me that many skills are not particularly useful at all (I currently have llms handling nearly 100% of my merge conflicts completely autonomously and I am happy to wave the white flag).

010