4 ms·
Heh… that approach is probably workable, but it sounds like such a hack to use two completely unrelated programming languages to get two different levels of saf
by comex 9y ago
Heh… that approach is probably workable, but it sounds like such a hack to use two completely unrelated programming languages to get two different levels of safety. It would be so cool if someone wrote a language/compiler which is to Rust as SPARK is to Ada.
- nickpsecurity 9y agoIt definitely is a hack. I've encouraged others with expertise to create SPARK-like tech for a Rust subset among other things. The problem is such experts are hard to find and it took SPARK 10-20 years to get to thus point. There's also a lot of verification tooling for C and Java especially that would have to be ported. So, I came up with a concept called Brute Force Assurance that tries to reduce verification from an expensive, expert problem to a pile of cheap labor problem. The idea is a language like Scheme or Nim expresses the algorithms in lowest-common denominator form that’s automatically converted to at least equivalent C, Rust, Ada, and SPARK. Their tools… esp static analyzers or test generators in C, borrow-checker in Rust, and SPARK’s prover… all run on the generated code. Errors found there are compared against the original program with it changed for valid errors. Iterate until no errors and then move on to next work item. Eventually, one might use certified compiler on one of these forms (probably C). What you think?
- zellyn 9y agoMakes sense. 1) Read "Beautiful Racket". 2) Implement it. :)
- pflanze 9y agoHey, this is an extension of what I'm planning to work on, which is a translator from Scheme enriched with lifetime and type information to Rust. See my comment here: https://news.ycombinator.com/item?id=15286945 https://news.ycombinator.com/item?id=15286945