Hacker News Reader

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.

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

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