4 ms·

> languages with good metaprogramming facilities let the users them to fit their needs. No amount of metaprogramming can fix the intractability of proving prog

> languages with good metaprogramming facilities let the users them to fit their needs. No amount of metaprogramming can fix the intractability of proving programs correct in the base language, especially if the metaprogramming facilities leak identifiers like a sieve (unhygienic macros). > userland extensibility can play a huge impact on the overall cleanliness of the language because new ideas can be tried out as libraries. Instead of (uselessly!) trying new language features, how about trying to find usable proof principles for the language features that you already have?

nickpsecurity 9y ago
"No amount of metaprogramming can fix the intractability of proving programs correct in the base language" It's actually rare people need to do proofs. If they do, they can also prove the programs correct with a tool suited for it like Isabelle/HOL or Coq then extract them to the desired language. It's worked for extractions to ML, Haskell, Scheme, and recently C (see below). https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.... There's also been verified LISP's (Scheme48, LISP 1.5) and metaprogramming constructs. So, it could be done in or for a LISP-like language with metaprogramming. I even found two metaprogramming schemes for Coq recently. https://popl18.sigplan.org/event/coqpl-2018-typed-template-coq https://popl18.sigplan.org/event/coqpl-2018-typed-template-c... https://hal.inria.fr/hal-01637063/document https://hal.inria.fr/hal-01637063/document That brings me back to an old idea I was just discussing with someone about SPARK. I've pushed for using all high-value/low-cost methods on highly-assured programs before using proof to avoid wasting time on stuff easy to prove wrong. Heavy hitters from Verisoft to Data61 have been coming around to that idea using Alloy and property-based testing of specs respectively. Many of these formal languages also have crappy tooling on FOSS side versus mainstream stuff. So, I suggested embedding them in something like Racket to: get the IDE and REPL benefits for productivity; use combo of Cleanroom-style development, Design-by-Contract, contract-based testing, combinatorial testing up to 6-way (3-way minimum), and fuzz testing with contracts running; extracting to Rust, C and/or SPARK w/ their static analyzers or model checkers run on that code; fix any problems in logic in original with repeats of that process as much as necessary; final result extracted to something with certifying compiler to knock out that risk. I called the concept Brute-Force Assurance given one just throws CPU power and low-cost labor at the problem without much specialist skill required past what DbC or SPARK needs. That combined with basic methods for high-availability or fault-tolerance plus recovery should make for one hell of a high assurance system at a fraction of the cost of formal verification. And if you wanted proof, then that system would already be nearly flawless to begin with in a structure (i.e. Cleanroom) amenable to easy proof with ability to extract to semantics of your choosing. If not Racket, I had K Framework used for KCC Executable Semantics for C in mind for formal alternative. Regardless, every tech I just cited (except SPARK) has low cost, lowers defects, and was easy to pick up. The combo should really bottom out defects without slowing time-to-market down too much to be useful. That's what formal proof did almost every time it was tried in normal development, esp if using 3rd party libraries.
- tluyben2 9y ago
  Did you ever progress that ‘old idea’; seems worth pursuing with some r&d grant?
  - nickpsecurity 9y ago
    Thanks. I didn't since I was still heavily researching the components I might use to design it. Previously, both temporal and concurrency errors were a problem to point that I might have had to integrate Java tooling, some commercial. That Rust knocked GC out of the equation makes it a lot more practical now for system-level code if whoever builds it can ensure the Rust and C code it generates are equivalent. The results on capability-secure, distributed languages such as Pony made me wonder if I should pause again to figure out a parallel or distributed by default version. However, I think we can tons of value out of something like a safe C with Racket expressiveness with the distributed stuff getting figured out over time. So, I'd like someone to try to build it with all I asked for being credit for the idea on top of a FOSS or free as in beer implementation for wide availability. We don't need another five-digit tool only enterprises can buy that taxpayer-funded R&D often goes to. (sighs) I might take a stab at it in the future, though. If not Racket, I was also looking at PreScheme, Red, and Nim for base languages. Main syntax, like Nim's, might need to be pleasant, though, so it will get adoption in first place with picky programmers. ;) Also, these days I recommend seemless compatibility with C data types or calling conventions so one can plug it into the C ecosystem without abstraction gaps or performance hits.
    - tluyben2 9y ago
      Can you mail me or I you? I believe I can make this work as open source and with enough funding.
      - nickpsecurity 9y ago
        Sounds good. I got your email. I'll respond within the week. :)
- catnaroek 9y ago
yogthos 9y ago
There's absolutely no evidence that formal methods approaches are effective in practice. These ideas have been around for decades, and they've only been found to be effective in a few niche areas such as compilers.
- skrishnamurthi 9y ago
  Ssh! Don't tell Amazon [http://lamport.azurewebsites.net/tla/amazon.html http://lamport.azurewebsites.net/tla/amazon.html], Facebook [https://research.fb.com/publications/moving-fast-with-software-verification/ https://research.fb.com/publications/moving-fast-with-softwa...], etc.!
  - yogthos 9y ago
    That's not empirical evidence that formal methods are more effective than other approaches. It just shows that the culture at these companies is conductive to using them. Walmart https://www.youtube.com/watch?v=av9Xi6CNqq4 https://www.youtube.com/watch?v=av9Xi6CNqq4 and Boeing https://www.youtube.com/watch?v=iUC7noGU1mQ https://www.youtube.com/watch?v=iUC7noGU1mQ etc use different approaches. :)
    - skrishnamurthi 9y ago
      You claimed "There's absolutely no evidence that formal methods approaches are effective in practice." and said the only real use was for compilers. I pointed out that they are effective in practice in domains completely unrelated to compilers. Your response is to bring up a totally different point ("more effective than other approaches" — a statement that can't even be falsified), talk mumbo about "culture", and point to Clojure talks, which is neither here nor there. In short, you are perfectly suited for "conversations" on the Web.
      - yogthos 9y ago
        How do you define effectiveness? A company using a particular approach does not automatically imply that it's an effective way to do it. You can make any approach work if you invest enough resources into it. To determine whether a particular approach is effective, it has to be compared against the available alternatives to determine whether it's effective or not. So, I'm a bit baffled by you saying that's a totally different point. So, perhaps you can explain the metric that you're using here to define effectiveness.

nickpsecurity 9y ago

"No amount of metaprogramming can fix the intractability of proving programs correct in the base language" It's actually rare people need to do proofs. If they do, they can also prove the programs correct with a tool suited for it like Isabelle/HOL or Coq then extract them to the desired language. It's worked for extractions to ML, Haskell, Scheme, and recently C (see below). https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.... There's also been verified LISP's (Scheme48, LISP 1.5) and metaprogramming constructs. So, it could be done in or for a LISP-like language with metaprogramming. I even found two metaprogramming schemes for Coq recently. https://popl18.sigplan.org/event/coqpl-2018-typed-template-coq https://popl18.sigplan.org/event/coqpl-2018-typed-template-c... https://hal.inria.fr/hal-01637063/document https://hal.inria.fr/hal-01637063/document That brings me back to an old idea I was just discussing with someone about SPARK. I've pushed for using all high-value/low-cost methods on highly-assured programs before using proof to avoid wasting time on stuff easy to prove wrong. Heavy hitters from Verisoft to Data61 have been coming around to that idea using Alloy and property-based testing of specs respectively. Many of these formal languages also have crappy tooling on FOSS side versus mainstream stuff. So, I suggested embedding them in something like Racket to: get the IDE and REPL benefits for productivity; use combo of Cleanroom-style development, Design-by-Contract, contract-based testing, combinatorial testing up to 6-way (3-way minimum), and fuzz testing with contracts running; extracting to Rust, C and/or SPARK w/ their static analyzers or model checkers run on that code; fix any problems in logic in original with repeats of that process as much as necessary; final result extracted to something with certifying compiler to knock out that risk. I called the concept Brute-Force Assurance given one just throws CPU power and low-cost labor at the problem without much specialist skill required past what DbC or SPARK needs. That combined with basic methods for high-availability or fault-tolerance plus recovery should make for one hell of a high assurance system at a fraction of the cost of formal verification. And if you wanted proof, then that system would already be nearly flawless to begin with in a structure (i.e. Cleanroom) amenable to easy proof with ability to extract to semantics of your choosing. If not Racket, I had K Framework used for KCC Executable Semantics for C in mind for formal alternative. Regardless, every tech I just cited (except SPARK) has low cost, lowers defects, and was easy to pick up. The combo should really bottom out defects without slowing time-to-market down too much to be useful. That's what formal proof did almost every time it was tried in normal development, esp if using 3rd party libraries.

tluyben2 9y ago
Did you ever progress that ‘old idea’; seems worth pursuing with some r&d grant?
- nickpsecurity 9y ago
  Thanks. I didn't since I was still heavily researching the components I might use to design it. Previously, both temporal and concurrency errors were a problem to point that I might have had to integrate Java tooling, some commercial. That Rust knocked GC out of the equation makes it a lot more practical now for system-level code if whoever builds it can ensure the Rust and C code it generates are equivalent. The results on capability-secure, distributed languages such as Pony made me wonder if I should pause again to figure out a parallel or distributed by default version. However, I think we can tons of value out of something like a safe C with Racket expressiveness with the distributed stuff getting figured out over time. So, I'd like someone to try to build it with all I asked for being credit for the idea on top of a FOSS or free as in beer implementation for wide availability. We don't need another five-digit tool only enterprises can buy that taxpayer-funded R&D often goes to. (sighs) I might take a stab at it in the future, though. If not Racket, I was also looking at PreScheme, Red, and Nim for base languages. Main syntax, like Nim's, might need to be pleasant, though, so it will get adoption in first place with picky programmers. ;) Also, these days I recommend seemless compatibility with C data types or calling conventions so one can plug it into the C ecosystem without abstraction gaps or performance hits.
  - tluyben2 9y ago
    Can you mail me or I you? I believe I can make this work as open source and with enough funding.
    - nickpsecurity 9y ago
      Sounds good. I got your email. I'll respond within the week. :)
catnaroek 9y ago

yogthos 9y ago

There's absolutely no evidence that formal methods approaches are effective in practice. These ideas have been around for decades, and they've only been found to be effective in a few niche areas such as compilers.

skrishnamurthi 9y ago
Ssh! Don't tell Amazon [http://lamport.azurewebsites.net/tla/amazon.html http://lamport.azurewebsites.net/tla/amazon.html], Facebook [https://research.fb.com/publications/moving-fast-with-software-verification/ https://research.fb.com/publications/moving-fast-with-softwa...], etc.!
- yogthos 9y ago
  That's not empirical evidence that formal methods are more effective than other approaches. It just shows that the culture at these companies is conductive to using them. Walmart https://www.youtube.com/watch?v=av9Xi6CNqq4 https://www.youtube.com/watch?v=av9Xi6CNqq4 and Boeing https://www.youtube.com/watch?v=iUC7noGU1mQ https://www.youtube.com/watch?v=iUC7noGU1mQ etc use different approaches. :)
  - skrishnamurthi 9y ago
    You claimed "There's absolutely no evidence that formal methods approaches are effective in practice." and said the only real use was for compilers. I pointed out that they are effective in practice in domains completely unrelated to compilers. Your response is to bring up a totally different point ("more effective than other approaches" — a statement that can't even be falsified), talk mumbo about "culture", and point to Clojure talks, which is neither here nor there. In short, you are perfectly suited for "conversations" on the Web.
    - yogthos 9y ago
      How do you define effectiveness? A company using a particular approach does not automatically imply that it's an effective way to do it. You can make any approach work if you invest enough resources into it. To determine whether a particular approach is effective, it has to be compared against the available alternatives to determine whether it's effective or not. So, I'm a bit baffled by you saying that's a totally different point. So, perhaps you can explain the metric that you're using here to define effectiveness.