Comments URL: https://news.ycombinator.com/item?id=49307383

Points: 33

# Comments: 20

So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.

It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.

In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.

It "features the development of the mathematical theory underlying a fictional ansible, a device capable of faster-than-light communication, which can send messages without delay, even between star systems." [1]

It doesn't get better than that. Certainly not "harder".

[1] https://en.wikipedia.org/wiki/The_Dispossessed

If you are interested in mathematics because it can model things precisely, and you want precise answers about these models, and you want to know how it is all connected (Langlands anyone?), AI is fantastic news. There is plenty of new and interesting and beautiful and elegant mathematics to be had this way, as well.

This is not a time to be scared or frightened. This is a time to be excited as fuck.

There will always be open questions. Now, there will be actually many more of them, because many more people will be asking questions.

[1] http://abstractionlogic.com

[1] https://www.wired.com/2010/06/iphone-4-holding-it-wrong/

The reported API costs for all of that would have been $180 though, which I cannot afford when the Fable promo ends on June 22nd. I am also a happy user of £89 Codex, it is really reliable and works very well, but Fable seems to be just noticeably smarter.

[1] https://zero.practal.com

See, the project actually has a well thought out structure that I design carefully, but more and more of it gets filled out by Codex. Codex is not smart enough to remember all the high-level design considerations, some of which had not been documented because I was just implicitly assuming them. So the fix was to use Codex to isolate the error, think about in terms of the high-level design, and fix the problem, which was partially an implementation problem, and partially a problem of the high-level design.

I fixed the high-level design with discussions with Codex, and documenting this, and then let Codex implement the fixes. The discussion took me more than an hour, the implementation was done in a few minutes.

This working style is similar to doing math: You have a high-level idea of what you are doing, and let that guide you, and Codex assumes the role of something that fills out all of the details you take for granted. Often it turns out your high-level idea had flaws, and this shows up in your code not working as expected. So you revise your high-level idea, refactor the code to reflect the modified high-level design, rinse and repeat.

Working this way is still really hard, but it allows me to do things I could not have done before. Getting your ideas validated (or refuted) in minutes instead of days is huge, and makes it possible to march through stuff that would have turned into a deadly swamp before, at least for me.

Now. Do I think that most corporate programmers will use Codex or CC in this way? I don't know, but I think probably not. So what will stop them going into the swamp until it swallows them, instead of backing up in time and marching around it?

It is also immediately clear why this plays a role in semantics for logics: although a ring is not that important in logic (I would think), the idea to study a theory through its syntactical consequences turned into semantics is very natural, and exactly what I do for abstraction logic as well, in particular via "valuation spaces". And it has the same property, once you set up everything the right way, things like completeness just automatically flow out of it.

In my book about abstraction logic (http://abstractionlogic.com) I have definitions, theorems, lemmas, and even observations :-) Just did a count of the frequency. Of course, not sure what those frequencies say about the relative importance.

-----------

Definitions 78

Theorems 20

Lemmas 76

Observations 41

Just saw that, and was thinking, wtf, really? Well... :-)

Comments URL: https://news.ycombinator.com/item?id=47626439

Points: 3

# Comments: 1

It can happen that the particular printing person on that day fucks up though.