On 5/25/23 10:00, Chuck Guzis via cctalk wrote:
On 5/25/23 08:58, Guy Sotomayor via cctalk wrote:
ADA and SPARK (a stripped down version of ADA) are used heavily in
embedded that has to be "safety certified". SPARK also allows the code
to be "proven" (as in you can write formal proofs to ensure that the
code does what you say it does). Ask me how I know. ;-)
I was aware of Ada's requirements in the defense- and aerospace-related
industry. Is that where your experience lies? Is SPARK the "magic
bullet" that's been searched for decades to write provably correct code?
I'm familiar with it from the higher end automotive perspective
(self-driving cars). Even when using C/C++ we have *lots* of standards
that we have to adhere to (MISRA, CERT-C, ISO-26262, etc).
The way SPARK works is that you have code and then can also provide
proofs for the code. Proofs are you might expect are *hard* to write
and in many cases are *huge* relative to the actual code (at least if
you want a platinum level proof).
--
TTFN - Guy
