4 ms·

It's basically a subset of Ada, so you can use it anywhere you'd use Ada. I don't think Lean is at a point that it's an Ada replacement.

adastra22 1y ago
Lean the math prover? What does that have to do with Ada/Rust?
- Jtsummers 1y ago
  > Lean the math prover? What does that have to do with Ada/Rust? I'm going to be rude, but there are 4 sentences in this thread and you appear to have not read two of them. The comment I responded to: >> I've never heard of SPARK. What advantages does it have compared to Lean? [emphasis added] The "It" in my response refers to SPARK.
  - adastra22 1y ago
    There was no need to be rude.
lenkite 1y ago
In a project, can you develop one module in Ada and another in SPARK and compile them together ? So, you can use safety-critical code in one module and regular Ada code in other modules ?
- Jtsummers 1y ago
  Yes, you can mix and match the two. This lets you do things like build a library with SPARK for some critical portion where you want SPARK's guarantees and can accept its limitations, and incorporate it into an application built with the rest of Ada.
  - lenkite 1y ago
    Oh lovely - need to put Ada on the learning plan. Formal languages were a bit of a drag because you needed to maintain a separate "specification" copy of your critical code. Going through Ada sample programs and surprised I can grok stuff without knowing anything about the language. Wondering why it never took off in the standard software world. Sure its a bit verbose, but so are Java and MacOS API's
    - Jtsummers 1y ago
      https://learn.adacore.com/ https://learn.adacore.com/ - I'd start here, good set of tutorials on the language including some comparative ones. It won't teach you everything you might need to know, but it's a free and good starting point.
    - Agingcoder 1y ago
      I think at least slow and expensive compilers back in the days, the defense and aerospace stigma, and in more recent times a common misperception that it’s closed source. And it’s never been cool stuff. And yes you’re right, it’s a very good language.

adastra22 1y ago

Lean the math prover? What does that have to do with Ada/Rust?

Jtsummers 1y ago
> Lean the math prover? What does that have to do with Ada/Rust? I'm going to be rude, but there are 4 sentences in this thread and you appear to have not read two of them. The comment I responded to: >> I've never heard of SPARK. What advantages does it have compared to Lean? [emphasis added] The "It" in my response refers to SPARK.
- adastra22 1y ago
  There was no need to be rude.

lenkite 1y ago

In a project, can you develop one module in Ada and another in SPARK and compile them together ? So, you can use safety-critical code in one module and regular Ada code in other modules ?

Jtsummers 1y ago
Yes, you can mix and match the two. This lets you do things like build a library with SPARK for some critical portion where you want SPARK's guarantees and can accept its limitations, and incorporate it into an application built with the rest of Ada.
- lenkite 1y ago
  Oh lovely - need to put Ada on the learning plan. Formal languages were a bit of a drag because you needed to maintain a separate "specification" copy of your critical code. Going through Ada sample programs and surprised I can grok stuff without knowing anything about the language. Wondering why it never took off in the standard software world. Sure its a bit verbose, but so are Java and MacOS API's
  - Jtsummers 1y ago
    https://learn.adacore.com/ https://learn.adacore.com/ - I'd start here, good set of tutorials on the language including some comparative ones. It won't teach you everything you might need to know, but it's a free and good starting point.
  - Agingcoder 1y ago
    I think at least slow and expensive compilers back in the days, the defense and aerospace stigma, and in more recent times a common misperception that it’s closed source. And it’s never been cool stuff. And yes you’re right, it’s a very good language.