5 ms·

I've never heard of SPARK. What advantages does it have compared to Lean?

by usamoi 1y ago

Jtsummers 1y ago
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.
OCTAGRAM 1y ago
They have different definitions of failure. In Lean a failure is to calculate wrong thing. In SPARK a failure is to not calculate at all because of memory issue or something like this. As far as I've seen SPARK, it encourages ephemeral data structures and effectful computations. Lean is less familiar to me, but I've got the impression that it is about correct computation in infinite memory and stack, and value-centered computations are encouraged. SPARK did not have pointers for long period. Then SPARK has got pointers, but only unique ones. Lean has shared pointers to immutable data structures. And infinitely recursive data structures. Yet another provable code I have found in Eiffel. There is "proven" doubly linked list in Eiffel. Something not possible in SPARK, going against unique pointers. Something not possible in Lean, going against immutability.

I've never heard of SPARK. What advantages does it have compared to Lean?

by usamoi 1y ago

I've never heard of SPARK. What advantages does it have compared to Lean?

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.

OCTAGRAM 1y ago

They have different definitions of failure. In Lean a failure is to calculate wrong thing. In SPARK a failure is to not calculate at all because of memory issue or something like this. As far as I've seen SPARK, it encourages ephemeral data structures and effectful computations. Lean is less familiar to me, but I've got the impression that it is about correct computation in infinite memory and stack, and value-centered computations are encouraged. SPARK did not have pointers for long period. Then SPARK has got pointers, but only unique ones. Lean has shared pointers to immutable data structures. And infinitely recursive data structures. Yet another provable code I have found in Eiffel. There is "proven" doubly linked list in Eiffel. Something not possible in SPARK, going against unique pointers. Something not possible in Lean, going against immutability.