5 ms·

> 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

> 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.
- ReleaseCandidat 2y ago
  Coq has "admitted" (or "admit"), but sorry is of course way better :). Lean also has "admit".
- dunham 2y ago
  Lean has `sorry` and Idris has `believe_me`. Recalling my math education, I would think the appropriate keyword would be `clearly`.
  - naasking 2y ago
    > Recalling my math education, I would think the appropriate keyword would be `clearly` I prefer the slightly more ominous "surely".
    - Nevermark 2y ago
      "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!

> 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.
ReleaseCandidat 2y ago
Coq has "admitted" (or "admit"), but sorry is of course way better :). Lean also has "admit".
dunham 2y ago
Lean has `sorry` and Idris has `believe_me`. Recalling my math education, I would think the appropriate keyword would be `clearly`.
- naasking 2y ago
  > Recalling my math education, I would think the appropriate keyword would be `clearly` I prefer the slightly more ominous "surely".
  - Nevermark 2y ago
    "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!