[usamoi]

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

[Jtsummers]

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.

[lenkite]

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 ?

[adastra22]

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

[OCTAGRAM]

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.