News for hackers. Stuff that matters.

rabarbers

Ask HN: Looking for a good course to learn proof assistant Lean 4

Hi HN, I’ve been exploring Lean 4, the theorem prover and programming language, and I’m impressed by what it offers for formal reasoning and proofs. However, it’s been difficult to find a structured, instructor-led course or organized study group (as opposed to just tutorials or documentation). Does anyone know of: University or online courses (open enrollment) teaching Lean 4 Any guided...

( Read More... | 4 comments | on HN )
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @05:32PM (#29423727)
Thanks for explaining! But how about this example:

  x:42
  {x+1}[5]
It results in

  6
It seems like you can define variables with the name 'x', but when you do not have explicit parameters, then the identifier 'x' is used to refer to the first implicit parameter, y - for second and z - for the third parameter. In context of implicit parameters x, y and z acts like predefined keywords.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @04:30PM (#29422930)
I tested and seems, that x is the first implicit parameter, y - second, z - third. It is as stated in their online documentation. When you try following example:

  {y+x*z}[1;2;3]
It gives result:

5

And in Q you cannot define implicit parameters with names, for example,: a, b, c. But You can define parameters explicitly:

  {[a;b;c]a+b*c}[1;2;3]
I still think that their implicit parameters are keywords. Similarly as keyword 'it' in Kotlin programming language is used to refer to the single parameter of the lambda expression.

In KatLang there are no predefined implicit parameter names. The user is the one who defines implicit parameters by declaring the implicit parameter names.

Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @12:26PM (#29419264)
A1 in Javascript pseudocode would be:

  function A1(x, y) {return x*y + x; }
But A2 would be:

  function A2(y, x) {return y*x + y; }
If you do not like the default order of implicit parameters, you can always use Grace~ operator to move x or y. Prefix form moves the parameter one position towards the beginning of the parameters list, postfix form moves one position towards the end of the parameters list:

  A1 = y~ * x + y
or

  A1 = y * ~x + y
or [Edit]

  A1 = y * x + y~
In the last example take into consideration, that without Grace~ operator y is the first parameter, so, you need to move it one position towards the end of the parameters list - therefore use postfix form of Grace~ operator.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @12:16PM (#29419091)
Can you explain the difference little bit more, Maybe using Javascript pseudocode as comparable example? I want to understand how Q is different from KatLang. The problem with me is that I do not know where I can try Q code, therefore I rely only on the documentation fragments I can find.
Re:Show HN: I built an online programming language on Thursday December 02, 2021 @10:35AM (#29417394)
Link to documentation is broken: https://codigo.so/docs/ (also link to community is broken, but I care more about Documentation link).
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @10:27AM (#29417264)
More specifically: the first unknown identifier becomes the first parameter for the closest algorithm defined with {} brackets. Properties (also called named algorithms) are defined as {} context. And KatLang program also is defined as {} context. I call it Second order algorithm - algorithms can contain another algorithms. First order algorithm is something defined between commas or semicolons. But inside brackets () or {} you can define second order algorithm.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @10:15AM (#29417124)
According to Q documentation, Q supports only 3 implicit parameters x, y, z: https://web.archive.org/web/20190213035913/http://code.kx.co...
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @09:50AM (#29416823)
Yes, the first unknown identifier becomes the first parameter, next unknown identifier becomes next parameter and so on...
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @09:26AM (#29416490)
Probably picking the term "perfect" was not the best think I could do. Seems, that others actively fight against it. I still believe that the perfect syntax has both attributes: 1) it is the shortest 2) it is expressive - you can express any expression in it. Picking that name made my life much more difficult.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @09:20AM (#29416396)
You need to carefully pick the right brackets () or {}. You can define an algorithm with both of the brackets, the difference is that () does not capture the parameter, but {} captures the parameter which is used inside the brackets. When You define a property, then property body is automatically interpreted as defined in {} brackets.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @09:12AM (#29416269)
I will do some research on APL and your mentioned 'commute operator', cannot comment on it now. But regarding languages: k/q the issues with them is that they use x, y and z as keywords for the parameters. x is always the first parameter, y - second, z - third. In KatLang parameter names are not predefined keywords, you can pick almost any parameter names you like.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @08:59AM (#29416146)
I am mainly inspired by C#. Ok, I can agree, that some things depends on the interpretation. You can think about several returned values as a tuple. In designing Algorithm concept, I was thinking how to decompose or deconstruct a mathematical function - to be able to operate with parameters, to transform input into output. Here You will say that it is the definition of function. Well, I went little bit further. In KatLang it is very important if you use brackets () or {}. Both brackets defines an algorithm, but () cannot hold implicit parameter. Maybe thinking from this perspective will help you see some more value in KatLang. What I wanted to say is that in KatLang I 'destroyed' or 'decomposed' mathematical function and used the parts to construct a concept that in KatLang is called an algorithm.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @08:47AM (#29416009)
I think, that there is needed Android app - calculator using KatLang syntax. That (or maybe iOS version) would make You care about it. I am planning to use KatLang syntax for physics tests in schools. Physics formulas can be defined using KatLang syntax. That is experimental idea, but I believe, that it can make a difference.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @08:42AM (#29415961)
Your OCaml function example looks like feature I call conditional parameters in KatLang (inspired from Erlang). In mathematics exists many different concepts which are called perfect. For example, perfect numbers. God called Lucifer a perfect. I provided a definition for symbols perfectness and tokens perfectness. You can call it unprofessional, but I did my best. I do not call my work perfect to make it more significant. I use term perfect as an attribute of the code expressions. Imagine identity function:

  function(x) {return x; }
In KatLang You can define it as:

  x
The question is: can you remove one more symbol without changing the meaning of the expression? If no, then, the identity function definition 'x' is symbols perfect according to my definition. Of course, I rely on the usage context and it allows me to hide some part of critical information and focus only on the short lambda expression.

Thanks for the elixir examples.

Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @08:15AM (#29415675)
Tuples require object deconstruction syntax. KatLang does not have object deconstruction feature. KatLang has simply deconstructed the function into input and output. In KatLang you define algorithms by specifying inputs and outputs. If You use implicit parameter, then the algorithm has an input. If You do not use implicit parameters, then the algorithm has only output and it is more like a data structure rather than a function.

I agree, that parameter ignorance operator # is ugly. I do not like it. The plan is to remove it in the future versions, but it requires some research.

About expression reading and parsing... Your argument is correct, but KatLang expressions are relatively short. I do not expect that KatLang will replace general purpose programming languages. KatLang is just a simple language for calculations. Main goal was to redesign the calculator and KatLang is good for that.

Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @07:25AM (#29415242)
Modern math syntax is relatively new, it started to form in 18th century. It is not too late to make some changes. Implicit parameters is only one feature in KatLang. Classic math functions can return only one value, that is why in KatLang there are no functions. In KatLang everything is an algorithm - concept which can return several outputs. Yes, some programming languages have syntactic sugar for that too, but still there are no accepted general syntax. Lambda is special case for an algorithm! Even natural languages have experienced a lot of changes. For example, Latvian language grammar changed in only 10 years. Maybe You are right about implicit parameters, but I believe, that implicit parameters are useful and I will try to convince the world about it. We will see how it will turn out ;).
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @07:04AM (#29415090)
It is not the same.

   A1 = x * y + x    
   A2 = y * x + x    
   A1(1, 2), A2(1, 2)    
returns results 3, 4 If You want to change parameter order, You can use Grace~ operator like this:

   A1 = x~ * y + x   
it moves parameter x one position towards the end of the parameters list.

Sorry, I do not know how to post code snippets in HN properly.

Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @06:58AM (#29415050)
When you have A=xy+x from math perspective it looks like assigning a value to a variable. When You use A(x,y)=xy+x it looks like math function definition. You can look at it as if used variable assignment syntax and changed underlying semantics to the function definition syntax. I suppose, people are familiar with classic math syntax and it will be difficult to change their beliefs. But I also believe, that smartphone usage can change people habits. When function body defines the function signature, it is much easier to move around the function definition on small screen devices, define function, edit, and so on... I advice to watch promotional video for KatLang predecessor - https://www.youtube.com/watch?v=ya8beSCx1IA It is still available on Windows Phone marketplace as IlCalculus app. Next goal is to develop Android app and I believe then it will be much easier to convince you, that implicit parameter declaration is the future feature of the clalculator.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @06:49AM (#29414995)
KatLang parser is executed as Blazor webassembly app on client side, therefore your entered KatLang code is not sent to the server. But I agree, it needs https, especially when KatLang supports operators like 'load' which can load KatLang code from other sources. Loading part is inspired from Prolog predicate consult.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @06:42AM (#29414947)
Page does not require any authentication and I wanted to make it simple. But too many people are asking about https, so I will configure https.
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @05:54AM (#29414641)
I was obsessed with the perfect syntax. Declaring method parameters in method parameters list is redundant, because the parameters appear in the method body anyway. This approach is not the best in all situations, but for short expressions, like lambda expressions, it is perfect (in my opinion). Check my paper on comparing lambda expression implementation: https://www.bjmc.lu.lv/fileadmin/user_upload/lu_portal/proje...
Re:Show HN: KatLang – Language for Calculations on Thursday December 02, 2021 @05:05AM (#29414361)
The author here. I am ready to answer any questions about KatLang. The future plan is to create android app and I hope that it will become the future calculator. I have been postponing android app creation for years, but now KatLang is in good shape and I can continue with tool development.
Re:Parsing: The Solved Problem That Isn't (2011) on Saturday October 25, 2014 @11:33AM (#8508464)
I started with udacity course: https://www.udacity.com/course/cs262 it teached how to build simple javascript parser.
Re:2014 Fields Medals announced on Tuesday August 12, 2014 @04:35PM (#8170003)
I do not understand why should HN be afraid to give reasonable reason for down voting. Looking at picture I also thought that Maryam Mirzakhani is man. I understood my mistake only by reading down-voted comments. Someone is spoiling valuable comments and it happens too often. Sad.
Re:Poll: I disagree with you, is it ok to downvote you? on Thursday August 07, 2014 @05:05PM (#8150125)
A) cultures are different and such subjective argument is not enough to use down-vote. If you are some smart ass who want something without emotions, go and chat with your PC, but if you are reading public opinions, do not be surprised that they are written by humans (probably containing some emotions). F) when someone makes something good and publishes it to be accessible by society it is normal to receive thanks, especially if it is open source project or non-commercial project aimed to make the world better. But suddenly some smart asses appears from nowhere with zero contribution, but with privilege to make other achievements invisible.

In my belief down-voting system is unfair. Especially if you are advised to shut-up when you are down-voted because it makes conversation boring... As HN does not stimulate responsible conversation, but only something like "say and shut-up if we do not like you", there are no reason for me to keep track of conversation and provide more arguments to prove that I am right.

Knuth wrote: soon USA will lose domonant positions. His prediction was wrong, which leads me to think that his oppinion about software patents was highly theoretical assuming how it would be if..., because he truly believes that... Such arguments are emotionally driven.

Ask HN: Do you need implicit parameters/arguments?

Article "Implicit parameters and implicit arguments in programming languages" can be found here:https://www.publicationservice.org/Artifact/ImplicitParametersYou are programmer, right? ;) So, you should understand what I am talking about… I would appreciate any feedback! If you prefer contacting by e-mail, you can write to: [email protected], if you can write something...

( Read More... | no comments | on HN )

Older »