|
|
|
|
|
|
by infogulch
782 days ago
|
|
|
I have no experience in this area, but when I last looked Lean and mm0 were the interesting theorem proving systems to me. Lean for its momentum and big projects, and mm0 for its goal of producing a minimal kernel proven down to machine code. Practal seems interesting and I scanned through the paper a year or two ago, but I have no reference point to evaluate it. I'm glad to see that you're still publishing about it. How would you compare Practal with Lean, and what do you hope to prove (ha) with the project? |
|
|
But the logic Practal is based on exists now. I am currently writing the basics of this logic up as a book [1]. Chapter 2 will be ready soon. I have learnt much about the logic in the last few months, also as a consequence of trying to implement it, and the book is based on this latest understanding. It all is really really simple, and I am trying to give it the proper form so that this becomes obvious.
I very much hope a first implementation is available this year, but this depends on how much I can work on it uninterrupted by money concerns.
In the end, what I am trying to prove with Practal is that formal logic doesn't make things more complicated. It actually makes things simpler.
[1] http://abstractionlogic.com