Re:Why not program right?
by nickpsecurity on Friday July 06, 2018 @08:08PM
(#17476051)
"Ada died off. "
On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.
I thought the legacy of Modula-3 lives in OpenJML (through ESC/Modula-3 -> ESC/Java -> ESC/Java2 -> OpenJML)? I have never heard anyone use it though.
Re:Why not program right?
by catamorphismic on Saturday July 07, 2018 @03:00AM
(#17477443)
> Rust had potential for proof work, but went off in a different direction.
Which direction is that?
C/C++ has too much undefined behavior. Ada died off. The scripting languages don't need it as much. Rust had potential for proof work, but went off in a different direction. There are modern proof systems, but they're rarely integrated with the programming language.