3 ms·

Curious but can we use lean4 as port target instead of Rust?

jon-wood 4mo ago
I'm sure its technically possible, you might need to provide a bit more context if you expect anyone to change course here and port it to a programming language approximately no one has heard of rather than Rust though. What makes you think that would be a good idea?
- koito17 4mo ago
  > approximately no one has heard of Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it. Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago. I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
  - HeavyStorm 4mo ago
    Oh, PhDs, you're right, that's not approximately no one... It's probably approximately one. I like Lean (and more generally dependent types) but ffs Lean has a very, very small userbase for a project like this. GGP would have to really justifyv the benefits for such a switch.
    - deleted 4mo ago
      [deleted]
    - jcelerier 4mo ago
      Apparently roughly ~150k math PhDs live on earth right now, assuming they all know Lean that's between 0.001% and 0.002% of earth population so quite closer to no one than one
bhy 4mo ago
I don’t think lean4 compiled code is as efficient as rust. For verification purposes, there are some tools allowing formal verification of rust code.
giancarlostoro 4mo ago
Never heard of it, and I nerd out on programming languages. Reminds me of a convo yesterday with my coworkers where I noted I never heard of Sheerpower a language someone who worked there had done, and I have heard of languages so old and niche most people are shocked. My first programming interview my interviewer was like what the heck are you doing with D? And he noted he has a room full of devs where nobody knows what D is.

I'm sure its technically possible, you might need to provide a bit more context if you expect anyone to change course here and port it to a programming language approximately no one has heard of rather than Rust though. What makes you think that would be a good idea?

koito17 4mo ago
> approximately no one has heard of Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it. Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago. I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
- HeavyStorm 4mo ago
  Oh, PhDs, you're right, that's not approximately no one... It's probably approximately one. I like Lean (and more generally dependent types) but ffs Lean has a very, very small userbase for a project like this. GGP would have to really justifyv the benefits for such a switch.
  - deleted 4mo ago
    [deleted]
  - jcelerier 4mo ago
    Apparently roughly ~150k math PhDs live on earth right now, assuming they all know Lean that's between 0.001% and 0.002% of earth population so quite closer to no one than one

bhy 4mo ago

I don’t think lean4 compiled code is as efficient as rust. For verification purposes, there are some tools allowing formal verification of rust code.

giancarlostoro 4mo ago

Never heard of it, and I nerd out on programming languages. Reminds me of a convo yesterday with my coworkers where I noted I never heard of Sheerpower a language someone who worked there had done, and I have heard of languages so old and niche most people are shocked. My first programming interview my interviewer was like what the heck are you doing with D? And he noted he has a room full of devs where nobody knows what D is.