practal

18 ms·

241.
by practal 4y ago
Very good points. It helps to list the requirements of a system before you actually build it! I did something very similar when I wrote about what I would like to see in an interactive theorem proving (ITP) system: https://doi.or
242.
by practal 5y ago
If you like to read about foundations, maybe you will like this as well: https://obua.com/publications/philosophy-of-abstraction-logi...
243.
by practal 5y ago
Very good point.
244.
by practal 5y ago
Economy of thought. In my opinion, subtyping declares a "is" relationship, and coercions declare a "can be viewed as" relationship. You would want both in Practal. Subtyping is more tricky than coercions in the sense tha
245.
by practal 5y ago
You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way undefinedness is handled in Practal. It is the most elegant way I can thi
246.
by practal 5y ago
I know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot add subtypes to a COC prover easily. [1]: https://link.springer.com&#x2
247.
by practal 5y ago
Good example why programming and logic are related, but not the same.
248.
by practal 5y ago
Very rarely, physists DO care about logic. For example: https://www.jstor.org/stable/1968621 And: https://en.wikipedia.org/wiki/The_Logic_of_Modern_Physics But given that the first is from 1936 an
249.
by practal 5y ago
It's important to sometimes step back and think about whether what you are doing actually makes sense. There are some assumptions about how formal logic is done in ITP (interactive theorem proving) systems that should be challenged. He
250.
by practal 6y ago
I am going to blog about the development of Practal as it goes on, but the blog will not have any comment section. Instead I will provide a link on each blog post to a corresponding HN submission. This way, anyone who feels like commenting,
251.
A Practical Logic(practal.com)
1 points by practal 6y ago|1 comments