3 ms·

Well, that list of languages got me interested. It'll be interesting to see where you're going with this. I think I'll check out the source a bit. I've been itc

by PeCaN 9y ago

Well, that list of languages got me interested. It'll be interesting to see where you're going with this. I think I'll check out the source a bit. I've been itching to hack on another GC for a while now. Thanks!

nickpsecurity 9y ago
The Show was a moderation error. It was just a submit. The list of languages got me interested, too, in whatever the author is doing. I posted it partly so people would see that list to hopefully get their own ideas. I imagine most tweaks of those languages would be of limited utility for large audiences much like most tweaks of LISP or OOP themselves. Yet, there might be some combination of features that's pretty amazing waiting to be discovered. I mentioned what I liked in the past with what metrics I wanted optimized in the future here: https://lobste.rs/s/hhmlfh/spry_language_inspired_by_rebol_lisp https://lobste.rs/s/hhmlfh/spry_language_inspired_by_rebol_l... The Brute-Force Assurance concept I've described scattered in different places to get most benefits of strong verification without cost and time drawbacks of needing specialists. I [probably] got idea from a mix of VMS or CLR's mixed-language development plus SRI attempt to convert proofs to every form to use their tooling. My concept was coding in language w/ metaprogramming and Design-by-Contract that can be converted into equivalent Rust, C, SPARK, and so on. Languages with lots of push-button-style tooling for finding or proving absence of defects. They all run on the code with anything found shown to developer to see if it's in original code. Rinse repeat until nothing found. If extracting to C, one can also use CompCert or Simpl/C for certified compilation with CPU's like CHERI optionally enforcing safety/security at machine level. Similar concept on spec side where structural and temporal properties might output a bunch of stuff like Alloy, TLA+, SPIN, Why3, or whatever to run against all of it at once. With it being a HLL w/ metaprogramming, it might allow a development cycle with quick iterations, REPL coding, whatever. At some point, each component is semi-frozen where developer starts annotating it to fire off the verification processes in the background as he or she works on the next component. Quickest analyses run first instantly reporting results so code is still fresh in mind. The app can follow gradual assurance philosophy similar to gradual typing with a mix of stuff in motion that's at least memory/concurrency/interaction-safe with dynamic checks covering what static ones can't plus things with tons of verification. At least, that's what's been tumbling around in my head for a while on this topic. There's a few works out there right now suggesting it might be more doable now than ever before. It would take some funding, some language lawyers, and people with knowledge of implementing such tooling.

by PeCaN 9y ago

nickpsecurity 9y ago

The Show was a moderation error. It was just a submit. The list of languages got me interested, too, in whatever the author is doing. I posted it partly so people would see that list to hopefully get their own ideas. I imagine most tweaks of those languages would be of limited utility for large audiences much like most tweaks of LISP or OOP themselves. Yet, there might be some combination of features that's pretty amazing waiting to be discovered. I mentioned what I liked in the past with what metrics I wanted optimized in the future here: https://lobste.rs/s/hhmlfh/spry_language_inspired_by_rebol_lisp https://lobste.rs/s/hhmlfh/spry_language_inspired_by_rebol_l... The Brute-Force Assurance concept I've described scattered in different places to get most benefits of strong verification without cost and time drawbacks of needing specialists. I [probably] got idea from a mix of VMS or CLR's mixed-language development plus SRI attempt to convert proofs to every form to use their tooling. My concept was coding in language w/ metaprogramming and Design-by-Contract that can be converted into equivalent Rust, C, SPARK, and so on. Languages with lots of push-button-style tooling for finding or proving absence of defects. They all run on the code with anything found shown to developer to see if it's in original code. Rinse repeat until nothing found. If extracting to C, one can also use CompCert or Simpl/C for certified compilation with CPU's like CHERI optionally enforcing safety/security at machine level. Similar concept on spec side where structural and temporal properties might output a bunch of stuff like Alloy, TLA+, SPIN, Why3, or whatever to run against all of it at once. With it being a HLL w/ metaprogramming, it might allow a development cycle with quick iterations, REPL coding, whatever. At some point, each component is semi-frozen where developer starts annotating it to fire off the verification processes in the background as he or she works on the next component. Quickest analyses run first instantly reporting results so code is still fresh in mind. The app can follow gradual assurance philosophy similar to gradual typing with a mix of stuff in motion that's at least memory/concurrency/interaction-safe with dynamic checks covering what static ones can't plus things with tons of verification. At least, that's what's been tumbling around in my head for a while on this topic. There's a few works out there right now suggesting it might be more doable now than ever before. It would take some funding, some language lawyers, and people with knowledge of implementing such tooling.