practal

13 ms·

181.
by practal 4y ago
I think philosophy is relevant to mathematics in the sense that one sometimes must be willing to step back from what one is doing, and ask deeper questions: Am I making assumptions here that are actually not true? This is a difficult thing,
182.
by practal 4y ago
That would not be a problem in Practal. That just falls into the non-executable subset. And all that means is that you have not set up equations that are executable and that handle this case. Actually, you could set things up so that this e
183.
by practal 4y ago
In Practal [1], you could declare the sum operator as \sum i. lower upper t[i] and then write the above sum as \sum i. 1 100 2 * i + 1 (after * and + and numbers have been defined as well) There is no reason why the above
184.
by practal 4y ago
Sussman is wrong. Happens to the best.
185.
Show HN: A First Look at Practal(practal.com)
2 points by practal 4y ago|0 comments
186.
by practal 4y ago
I see you are starting from what you want it to look like. That's a good idea! Did the same for Practal [1]. You might be interested in trying to express your language within Practal. Within the next 1 to 2 weeks something you can star
187.
by practal 4y ago
To be honest, I am quite amazed by how nicely all the pieces are coming together now. It all just feels right, it feels like collecting fruit from under a huge apple tree.
188.
by practal 4y ago
Thank you! Yes, a large part of programming will be just a special case of doing mathematics.
189.
by practal 4y ago
Very interesting read. Also very timely for me (I am always amazed how HN often has posts that resonate strongly with what I am currently doing), as I am just now designing a programming language based on a generalisation of Algebra, which
190.
by practal 4y ago
Yes, I know. The reason why you call them "frameworks" instead of logics is because they don't have a model-theory based semantics, but are justified via proof theory. Abstraction logic on the other hand is a logic with its o
191.
by practal 4y ago
Lean is well engineered, is also marketed as a programming language, and expressive enough to do proper math in it. Type theory is more elegant to implement than set theory based on first-order logic. That's about it. Nevertheless, fir
192.
by practal 4y ago
You are probably confusing "automation" with "mechanisation" here, and maybe also with "computing". It is very easy to automate set theory, at least when it is just embedded in first-order logic, and at least c
193.
by practal 4y ago
Brilliant idea. I am actually just researching how to build my own structured document editor for the web, based on my parsing engine for Pyramid grammars, and I'll certainly examine how to apply this idea in my context.
194.
by practal 4y ago
"An Algebraic Approach to Non-Classical Logics" by Helena Rasiowa was an eye-opener for me. Before that, "A short introduction to intuitionistic logic" by Gregory Mints is a great read which introduced me to Kripke model
195.
by practal 4y ago
I would say the most important idea in math is logic. Of course, fix points do play an important role in logic as well. For example, Cantor's theorem means that it really makes no sense when studying a mathematical universe, to try to
196.
by practal 4y ago
So according to you, Feynman did it poorly? Seems to me then being a poor philosopher is a good thing.
197.
by practal 4y ago
Here is my pretty unphilosophical take on the philosophy of mathematics: https://obua.com/publications/philosophy-of-abstraction-logi... Why should you read it? Because it introduces and explains the best logic known t
198.
by practal 4y ago
I am pretty sure that in 20 years every mathematician will happily use an ITP system. That is because formal reasoning is not unnecessary, but just too burdensome to be done on paper. Ideally a future ITP system will give you the formalisat
199.
by practal 4y ago
That depends on the ITP system. But in general, in an ITP system you can separate the name of something from how it is displayed. In the ITP system I am currently building, Practal, the displayed syntax does not need to be unique. So choosi
200.
by practal 4y ago
I would say it covers naming things and cache invalidation. And it is really really good at avoiding off-by-one errors.
201.
by practal 4y ago
About 8 to 9 years ago I asked Michael Nielsen (one of the authors of this PDF) by email what he thinks about interactive theorem proving. He was kind enough to answer, and replied something along the lines of that he doesn't believe m
202.
by practal 4y ago
I think this is great stuff. I have been thinking very much along these lines for a few months now as well, as a user interface for a logic I discovered. In the end, TeX does something very similar, just with a sharp focus on typesetting. I
203.
by practal 4y ago
I can totally relate to that. That's how I arrived at Abstraction Logic [0]: Banging my head against the wall (no, not literally), until something gave and I could suddenly see the most simple and powerful logical kernel possible. This
204.
by practal 4y ago
Very interesting. I did never really look at the "Concrete Mathematics" book, so I missed this take by Knuth on turning a formula F into a term [F] by defining it as 1 if F is true, and 0 if F is false. Note that this cannot be do
205.
by practal 4y ago
Depends on the language. Since this year I am getting up to speed with JavaScript and TypeScript, and there are a lot of different notions around to learn. It really clicked for me just recently when I implemented my own little unit testing
206.
by practal 4y ago
You can do whatever you want. You just need to prove that it is correct. I guess I wasn't as clear as I hoped I would be. I don't think the Array indexing issue can be dealt with by (just) improving its interface specification. I
207.
by practal 4y ago
You will notice that you use the array the wrong way when you try to prove the correctness of the client of the array. Somewhere in the specification of the client it will be required to, let's say, sum up all of the elements of the ar
208.
by practal 4y ago
Thank you for this explanation! In a way that is what I said: The problem is not that the types did not fit, the problem is that the code did just not behave as expected according to the interface specification. And combining many different
209.
by practal 4y ago
As far as I understand the situation the problem is that you do NOT always get type errors during runtime. Instead, you just get a wrong result, because the combination is legally allowed (that means, the types are accepted), but has not be
210.
by practal 4y ago
I think it is specific, because a) Julia is a dynamic language, and b) it uses dynamic multiple dispatch. I think these features are great, but on their own they lead to exactly the situation as described.

More ›