Hacker News new | ask | show | jobs
by whytevuhuni 201 days ago
I'm a Rust fanatic but probably not an activist. I am curious about Ada / SPARK though.

From what I've seen, taking on SPARK means taking on full verification, close to what seL4 is doing. Doesn't that make it extremely difficult to use for larger projects? My understanding is that seL4 is an absolutely heroic effort.
1 comments
GhosT078 201 days ago
Ada is very scalable, suitable for everything from blinking LEDs on an AVR microcontroller board to controlling interplanetary spacecraft. Similarly, SPARK can be used incrementally, proving lower level or critical parts first.
link
whytevuhuni 201 days ago
How does this SPARK/non-SPARK mix compare to Rust's safe/unsafe mix though, in terms of both safety and pragmatism for larger non-interplanetary software? Like, for creating a CLI tool, a GUI application, a game, a web server?
link