Hacker News Reader

Comment by 6gvONxR4sf7o | Hacker News Reader

I wish one of these languages (where you can prove and confirm that your code follows the formal spec) would aim for production use. I was really interested in Lean 4 when I found out that it aims to be a general purpose language, but then I saw that the language manual still has a section titled "Should I use Lean?" that emphasizes it's just a research project not a product and still expects a bunch more breaking changes, and so on.

Some day, I'd love to write proofs instead of tests in some places.

View on HN

While I agree with that in principal, in talking to people who have actually written proved programs I get the impression they don't think it is practical to prove programs that are more than medium sized. I'd love to prove my code correct, but I deal with 10s of million lines of code and nobody has a clue how you would approach a problem that large (we use C++, but you can select a different language if you want - the problem is the size and you can't get around that with a different language

Surely it wouldn't be aimed at proving a 10 million line black box of code, right?

In my mind it would have to be built from the ground up, sub unit tests for function proofs and maintain 100% coverage as you go along. As long as the constituent parts are proven you don't have to zoom out to a macro level.

Divide and conquer does work a bit, though. Languages that support strong encapsulation of various structures will be easier to work with than those that pass pointers around.

As an example, having proofs of various properties of strcat, strcpy, etc. will help less in large programs than having proofs for all Java’s methods on String. In the former, you’ll also have to proof that covers all accesses to your data. In the latter, the JVM guarantees that.

I talk to folks who are involved in proof engineering and they disagree here. It is possible to prove large systems when you have good automation. But perhaps it's writing the automation that is hard right now due to a small overlap in skills.

Writing the proofs is one thing but writing the automation that scales those proofs to a larger system and which makes it easy to extend the system without breaking the proofs constantly is key and requires more "engineering" focused people rather than proof-focused ones.

I've talked to people on both sides of that question. Some think you can (but have had little success in convincing anyone to do it), others think you cannot.

> Some day, I'd love to write proofs instead of tests in some places.

Believe my, you only want to do that if the proof assistent accepts "I leave the details as an exercise to the reader" ;)

I do a lot of work with Isabelle, and when doing proofs, you can use the word "sorry" to basically say "this is true because I said it's true okay".

It's become a running joke in my grad school of "when in doubt, there's always 'proof by sorry'".

I'm not as familiar with a lot of the other proof assistants but I suspect there are similar constructs?

> I do a lot of work with Isabelle, and when doing proofs, you can use the word "sorry" to basically say "this is true because I said it's true okay".

I always thought that unsafe { .. } blocks in Rust should be called trustme { .. }

But sorry { .. } is even better!

Yeah, it's pretty funny to see the first draft of anything I'm trying to prove; it'll be polluted with sorry's everywhere; it comes off as the most apologetic, completely un-confident bit of math you can think of.

The worst part is when you forget to remove a sorry (or three) because of a linked file you didn't check, and you submit stuff to other people on the team thinking you discovered something pretty cool, only to find out that you didn't actually prove anything.

My favorite is accursedUnutterablePerformIO https://hackage.haskell.org/package/bytestring-0.12.1.0/docs...

    This "function" has a superficial similarity to unsafePerformIO but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the IO monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet.

Coq has "admitted" (or "admit"), but sorry is of course way better :). Lean also has "admit".

Lean has `sorry` and Idris has `believe_me`. Recalling my math education, I would think the appropriate keyword would be `clearly`.

> Recalling my math education, I would think the appropriate keyword would be `clearly`

I prefer the slightly more ominous "surely".

"Obviously" casts a nice aspersion upon anyone so uncouth as to question its validity.

Of course, any junior member of a team that is willing to stand up and state that, no, the assertion is anything but obvious to them, should get an immediate promotion, and be quickly moved to another group!

Well Coq is used to build a C compiler used in aerospace. At the very least you could write "trricky" stuff in that, and then use the compiled artefacts in your toolkit.

I get the general complaint, though. I wish I could have the syntax-based interactive proof system everywhere.

I wonder how that is compatible with the industry requirements, and even with software engineering in general. A lot of the code we write is short lived, either because we're iterating, or because features aren't used anymore. Also, bugs aren't the end of the world most of the time. You don't aim for 100% correctness, but for something that provides value to users and it's better than your competitors. Formal proofs may be useful in some case, but I don't see them outside very niche fields. Even regular static types can be argued against.

Code written in F* is running in Firefox, Linux, Windows, and Azure: https://project-everest.github.io/.

Cool! Thanks for the link.

It seems a practical system would do all of the above:

- attempt a proof, could pass or fail, but if it times out, then fall back to...

- property-based test case generation, using logical statements and data generators, shrinking, etc.; many will pass, some will fail, but if some time out ...

- generate simple tests, and edge cases, which may trivially pass, but could be edited by hand to become more useful

If you add a timeout, then exponential runtimes, and even the Halting Problem, always give an answer, even if the answer is to try something simpler.

For small projects without tight performance or reliability requirements, Lean 4 is fine. It is lacking a lot in basic I/O functions, but you just yank them directly from the C standard library via the FFI and use them in your code. Don't expect to be able to prove anything about your code, though; just treat Lean as a pure functional language like Haskell but with dependent types and eager default evaluation.

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them.

[Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect LISP style ergonomics here. It doesn't help that the meta-programming book shows some trivial examples of macro rules and then delves deep into proof tactics for the next 2 chapters, leaving the reader who wants general code transformations stranded].

In order to use Lean for proving properties for serious amounts of code, you need to write an entire tactics library similar to mathlib (but for code). Nobody has done this. Maybe it is reasonably hard, or maybe unreasonably hard; the point is, there is no serious collaborative effort that I know of.

Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?

Probably, from what people are telling me. But Coq is not a general purpose language, it is a dedicated theorem prover. I don't use Lean as a theorem prover for code (only for mathematics) and I myself don't do any code formalization unless someone offers to pay me.

The reason I code in Lean is because I find it fun, and I think it is a very nice general purpose language; for instance, I like Lean much better than Haskell. If Lean ever gets the libraries Haskell has, I will be really excited.

I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?

I prefer Lean to Haskell (never said Lean is a better language) for fairly shallow reasons really:

- I like Lean's inductive type system much better that Haskell's,

- I prefer eager evaluation by default,

- I like the syntax better,

- I like dependent types; they are dangerous, but it is great to have the option.

I suspect some people may also prefer Lean's macro system to Haskell's, but I haven't worked much with either, so I don't know about that.

Out of curiosity, have you tried Idris? It would tick at least boxes 2 and 4, while possibly being a little bit more geared towards general programming.

Reply on news.ycombinator.com