[practal]

Well, the most important difference is that Lean exists and is going strong, and Practal doesn't even exist yet.

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