Comment by agentultra | Hacker News Reader

Comment by agentultra | Hacker News Reader

A regret: never being able to afford university and always feeling like it was too late when I finally could.

It turns out I really enjoy type theory, category theory, and formal mathematics. I also care about liability, reliability, and safety. And all I can do is study in my own time, which I do freely, in order to catch up. And I will never get a research position or work at a startup where I can put these skills and ideas to the test.

Oh well. I will still work on the libffi integration in the community Lean fork and will try to get Lean working on AWS Lambda and GCP, etc.

If you're younger and starting out -- don't neglect maths! It is far more useful than the programming language du jour. The former is how you weather the constant flux of the latter. And how you solve hard problems.

Interesting point, reminds me of this article: https://www.supermemo.com/en/archives1990-2015/articles/geni.... One of the points it makes is basically that abstract thinking is more valuable than specific facts, and that math is basically the king of this. I hadn’t really thought about comparatively weak something like programming can be since a strong focus of it is syntax (if programming and computer science are somewhat seperated).

I would agree that the ability to think abstractly is a fundamental skill to designing systems using software. Maths is a good tool for this and it has aided engineers and scientists for centuries.

Can you tell me more about your project to get lean working on the cloud providers?

Sure!

The high level goal is being able to write proof-carrying code in more places.

I think it's important for us to be able to guarantee properties/requirements of our programs and one way to do that is with formal methods. Lean is not only a proof assistant but also a dependently typed pure functional programming language with a decent VM. I would like to be able to ship the program from the proof.

I'm starting from the low level of the Lean VM by adding libffi support so that we can write high-level bindings to C libraries and bootstrap the Lean ecosystem. We need libraries to call databases, parse JSON and other serialization formats, speak HTTP, etc. The goal is to be able to ship an AWS Lambda function written in Lean.

Sounds very cool. Is there any way to follow your progress?

Reply on news.ycombinator.com