Hacker News Reader

Comment by yogthos | Hacker News Reader

Instead of having to think about every possible way a language might be used and account for it up front, languages with good metaprogramming facilities let the users them to fit their needs. This way the core language can stay small and focused while remaining flexible.

While you don’t want everybody building their own language, userland extensibility can play a huge impact on the overall cleanliness of the language because new ideas can be tried out as libraries. If these ideas don’t pan out, the community moves on. Projects using these libraries will keep working, but the core language doesn’t end up accumulating cruft. I wrote about that in detail here: https://yogthos.net/posts/2017-10-03-MovingForwardByLettingG...

View on HN

...which is why Scheme has, like, 37 different, incompatible object systems.

Everything has costs.

That's Scheme. Lisp, meanwhile, has one: CLOS. One is excellent for learning about things like hand-rolled object systems, and one is excellent for building large systems.

Common Lisp has CLOS. I'm aware some purists don't think Scheme is a Lisp but, regardless of one's stance on this, there are most definitely other Lisps than Common Lisp.

Having called the result of Lisp standardization ANSI Common Lisp instead of just ANSI Lisp doesn't change the fact that the whole effort was all about standardizing Lisp.

Moreover, why not just say Scheme or Clojure when talking about Scheme or Clojure?

If ANSI C had been called ANSI Common C, would Java fans never cease to insist on calling Java a dialect of C?

> the whole effort was all about standardizing Lisp

There are more Lisps now than ever, so perhaps that was not as successful as was hoped.

> why not just say Scheme or Clojure when talking about Scheme or Clojure?

Why not just say "Common Lisp" when you mean Common Lisp, and "Lisp" when making true general statements that include other things that have always been considered Lisps? How are we to refer to Emacs Lisp without tying ourselves in knots if we refuse to say that "Lisp" includes it?

You say that, but SLIB [0] is the canonical place to go with Scheme, which has the "Macroless Object System" [1], based on CLOS from Common Lisp.

SLIB is included with Guile, and compatible with almost all Schemes. If a Scheme has an object system inbuilt, it is likely to be built around SLIB's.

[0] https://people.csail.mit.edu/jaffer/SLIB

[1] https://people.csail.mit.edu/jaffer/slib/Object.html#Object

Sure, it's not a guarantee that the language will stay small and focused, but it provides a path towards that. Clojure has been around for a decade now, and the core language has grown very little. I think it helps that Clojure is a BDFL driven language as opposed to being a design by committee.

> 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?

"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....

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-c...

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.

Did you ever progress that ‘old idea’; seems worth pursuing with some r&d grant?

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.

Can you mail me or I you? I believe I can make this work as open source and with enough funding.

Sounds good. I got your email. I'll respond within the week. :)

> 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).

It baffles me that people think they can solve the problem of the intractability of systems by piling up more complexity on top.

> There's also been verified LISP's (Scheme48, LISP 1.5) and metaprogramming constructs.

It doesn't make sense to “verify language features”. What you verify is programs. Of course, the Lisp crowd is fundamentally incapable of distinguishing definitions from implementations, which leads to this regrettable sort of mistake.

> So, it could be done in or for a LISP-like language with metaprogramming. I even found two metaprogramming schemes for Coq recently.

This fails to address my original comment. Have you actually understood it? The point was (and still is) this: “Metaprogramming might write half of your program for you, but it won't help one iota with the proof of correctness unless the base language is already something mathematically nice to work with.” The excessively operational definition of pretty much every Lisp dialect in existence makes it prohibitively expensive to formally analyze the humongous swathes of code generated by Lisp macros. The problem with Coq is, surprisingly for something coming from the type theory crowd, exactly the same: You can't really understand a Coq proof script just by reading it. Instead, you have to replay it. Operational thinking does not scale.

> That brings me back to an old idea I was just discussing with someone about SPARK. (...)

This sounds insanely complicated. The only justification I can come up with for this kind of thing is manager thinking: “This process has lots of steps and makes people's lives miseable, hence I must be doing something right!”

"It baffles me that people think they can solve the problem of the intractability of systems by piling up more complexity on top."

The systems that ran for over a decade without downtime weren't done by formal proof: they had lots of review, checks and redundancies that came from prior experience with failures. Tandem NonStop comes to mind with VMS clusters getting pretty far. Identify a problem, develop a mitigation that works for all inputs, review it, test it, and deploy. Integrate with careful review and thorough testing. Whereas, a number of systems that were "proven" have failed after basic review or testing. Proof is just one tool among many instead of anything to think of as necessary or perfect.

Far as empirical evidence, those prior systems plus current ones with the most uptime or correct functioning in industry didn't have formal proof or use languages you'd recommend. That shows they're not necessary to achieve that goal. Formal proof with realistic models indeed showed the highest level of correctness once the tools matured. The drawbacks were: cost was insanely high, the models required overly-simplistic implementations, and time-to-market put them behind competition which can kill a company in markets. So, I recommend most don't do that kind of stuff. Whereas, I recommend CompSci do a mix of developing productivity/maintenance boosters (eg Racket, refactoring aids), optimizations, push-button tooling for verifying apps in popular languages (eg Pathfiner, Astree Analyzer) and clean-slate, verified stuff like miTLS or CompCert that can see real-world use without requiring specialists. Gotta balance across what people care about.

"The excessively operational definition of pretty much every Lisp dialect in existence makes it prohibitively expensive to formally analyze the humongous swathes of code generated by Lisp macros. "

The simplicity of it should make a SPARK-style analysis easy if the meta eventually decomposes into simple functions or operations with contracts describing intended structure or value ranges. The macros themselves can also be proven to be certified generators. Anyway, I think it's easier to address your point by comparing the base language to LISP in terms of ability to write a formal semantics or easily analyze it. Most mainstream languages fail immediately. A subset of LISP is doable given ACL2, VLISP and Myreens work. SML seems to win overall since it was designed for this but looses on many practical fronts like performance, developer tooling, and library ecosystem. Ocaml subset is closest to the goal for ML's but still behind mainstream stuff on factors more important to developers. Maybe Haskell, too, given verification tooling for it I've seen but I don't know its semantics so can't say more.

In any case, you'd be trading everything that gives developers velocity on software development for the ability to formally prove something more easily in the language which 99.999% of developers won't do. They can reach higher than their QA goals without it using lightweight methods with empirical proof of effectiveness above. Also, 99+% of proof engineers won't care about provability of base language either since they prefer to use dedicated tools with an extraction (eg CompCert) or equivalence check (i.e. seL4). If real-world deployment, people wanting a proven component can also prove it down to ML, C or ASM to wrap with a FFI (eg miTLS pieces in Firefox) or hide it behind an API (eg MULTOS CA in SPARK/Ada/C++ mix). Things like linking types by Patterson and Ahmed will make that safer over time.

"This sounds insanely complicated. The only justification I can come up with for this kind of thing is manager thinking: “This process has lots of steps and makes people's lives miseable, hence I must be doing something right!”"

I already gave you the reason: get confidence or defect rate close enough in practice to formal proof that software will meet its specification or fail safe taking developer right to error... without costs or time-to-market impact of formal verification. At most, we might be talking one well-trained, median programmer added per team instead of a proof engineer. Managers barely care about software quality on average much less formal proof. Selling them on improving defect rates at low cost in ways that makes extensions or maintenance easier is much more likely to succeed. Good example below by a Lockheed person on Design-by-Contract comparing it to other methods:

https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

We've worked on Racket + Alloy for ~8 years now, including using the Racket REPL for similar purposes. And built several tools with it (e.g., for networking analysis). Email me (sk@cs.brown.edu) if you want to chat more.

I knew I recognized you: typing your name brought your page up immediately. I had previously posted your ADsafe work in a lot of places interested in how to do JS better. Just posted Pyret on Lobste.rs with them enjoying that. Didn't know you worked on that, Racket, and theorem provers. Neat stuff in your publications. :)

Yeah, I'll probably email you this week or the next.

Thanks kindly. Will look forward to chatting.

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.

Ssh! Don't tell Amazon [http://lamport.azurewebsites.net/tla/amazon.html], Facebook [https://research.fb.com/publications/moving-fast-with-softwa...], etc.!

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 and Boeing https://www.youtube.com/watch?v=iUC7noGU1mQ etc use different approaches. :)

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.

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.

Reply on news.ycombinator.com