3 ms·
Can you tell me more about your project to get lean working on the cloud providers?
by joycian 7y ago
Can you tell me more about your project to get lean working on the cloud providers?
- agentultra 7y agoSure! 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.
- joycian 7y agoSounds very cool. Is there any way to follow your progress?