3 ms·

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

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.

bluGill 2y ago
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
- PhunkyPhil 2y ago
  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.
- Someone 2y ago
  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.
- agentultra 2y ago
  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.
  - bluGill 2y ago
    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.
ReleaseCandidat 2y ago
> 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" ;)
- tombert 2y ago
  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?
  - nextaccountic 2y ago
    > 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!
    - tombert 2y ago
      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.
    - ReleaseCandidat 2y ago
      My favorite is accursedUnutterablePerformIO https://hackage.haskell.org/package/bytestring-0.12.1.0/docs/Data-ByteString-Internal.html#g:10 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.
ykonstant 2y ago
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.
- nequo 2y ago
  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?
  - ykonstant 2y ago
    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.
    - nequo 2y ago
      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?
      - 2y ago
yodsanklai 2y ago
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.
rtpg 2y ago
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.
amw-zero 2y ago
Code written in F* is running in Firefox, Linux, Windows, and Azure: https://project-everest.github.io/ https://project-everest.github.io/.
- 6gvONxR4sf7o 2y ago
  Cool! Thanks for the link.
mikhailfranco 2y ago
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.

bluGill 2y ago

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

PhunkyPhil 2y ago
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.
Someone 2y ago
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.
agentultra 2y ago
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.
- bluGill 2y ago
  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.

ReleaseCandidat 2y ago

> 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" ;)

tombert 2y ago
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?
- nextaccountic 2y ago
  > 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!
  - tombert 2y ago
    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.
  - ReleaseCandidat 2y ago
    My favorite is accursedUnutterablePerformIO https://hackage.haskell.org/package/bytestring-0.12.1.0/docs/Data-ByteString-Internal.html#g:10 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.

ykonstant 2y ago

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.

nequo 2y ago
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?
- ykonstant 2y ago
  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.
  - nequo 2y ago
    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?
    - 2y ago

yodsanklai 2y ago

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.

rtpg 2y ago

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.

amw-zero 2y ago

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

6gvONxR4sf7o 2y ago
Cool! Thanks for the link.

mikhailfranco 2y ago

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.