Viewing profile — practal

Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic. So this is not because of the logic,…

> So you get complex recursion and inductive definitions baked into the kernel. It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now…

I added proof objects ages ago to HOL Light, it is not a big deal. It's just, as Larry said, why would you want them in the first place?

So what happens with optimistic local operations that become invalid after replay of canonical operations? Are they just thrown away as well?

One of my favourite books of all time is by her: The Dispossessed. It "features the development of the mathematical theory underlying a fictional ansible, a device capable of faste…

I actually think it is just the dawn of mathematics. During the last few days I discussed a few questions about abstraction logic [1] with AI that I was wondering about for quite s…

I think 6) is a very good point. The simple reaction to it is, well, I just define a small verification kernel that I trust, and the rest is just scaffolding that does not need to …

TU Munich and Nipkow, Makarius et.al. are also at the center of the influential Isabelle theorem prover. TU Munich is cool :-)

I agree with that, that's why I am starting with plain syntax first in https://zero.practal.com , because that is really where all the information/logic lives. But there will also …

How did you get suspended for 8 hours, given a 5-hour window? Maybe you are prompting it wrong [1]. [1] https://www.wired.com/2010/06/iphone-4-holding-it-wrong/

I used it yesterday afternoon-night and this morning-afternoon, UK time, over a period of a few 5-hour windows. I didn't count the prompts, wall time was 1d6h, API time was 2h10m.

I am quite impressed with Fable 5. I used the £18 subscription, and asked it to convert the document processing of Practal Zero [1] from running in the same thread as the UI to a w…

To add, what also often happens in these discussions is that Codex suggests a design that makes no real sense at all, or that it brings up two or three design alternatives, and rec…

On Saturday I thought I had vibe coded myself into a mess. I had implemented a new block type in my structured editor for Practal Zero (or rather let Codex do it), and suddenly the…

Super. I always wanted to learn about sheaves and schemes and the like, and this gives a simple introduction that really motivates digging deeper into the details. It is also immed…

> Even more important than lemmas are observations, but that is another story. In my book about abstraction logic ( http://abstractionlogic.com ) I have definitions, theorems, lemm…

> After mass feedback from the public, we're excited to announce that AXLE is switching from Lean to Rocq. The new name will be AXRE (Axiom Rocq Engine). All existing Lean proofs w…

Print-on-demand Amazon paperback books can have great quality. It is mainly the responsibility of the author, by doing proper layout, and choosing a nice paper option. I've self-pu…

Just two days ago I was curious about the PhD advisor of my PhD advisor and so on, and discovered that I am actually an academic great-grandson of Hoare (shame on me, I should have…

I think that is a very good point. Code is definitely not worthless, but I don't think that capitalism has the right tools for pricing it properly. I think it will become a lot lik…

I see the current generation of AI very much as a thing in between. Opus 4.5 can think and code quite well, but it cannot do these "jumps of insight" yet. It also struggles with st…

In principle, this is how these systems work. In practice, there are usually plenty of things that make it difficult to say for sure if you have a proof of something.

You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I wa…