I can’t believe that I can prove that it can sort

Re:I can’t believe that I can prove that it can sort by ufo on Monday July 04, 2022 @08:59AM (#31976541)

The comments so far have tended to focus on the proof itself, but for me the coolest part of the blog post were the formal methods.

Does anyone here also use SPARK for this sort of thing? Are there other formal methods tools you'd use if you had to prove something like this?

[ Parent | on HN ]

Re:I can’t believe that I can prove that it can sort by im3w1l on Monday July 04, 2022 @12:28PM (#31978846)

Yeah, I see this as a very interesting reply to the TLA+ post. Might spend my evening diving into Ada and Spark.

Edit: Some things I noticed. The package gnat-12 does not have gnatprove. Ada mode for emacs requires a compilation step that failes with gnat community edition. With alire there is no system gnat so it cannot compile it (quite possible I'm missing something). In the end I gave up on using emacs. Gnatstudio wouldn't run for me until I realized it needed ncurses. It also had some unhandled exceptions for me (raised PROGRAM_ERROR : adjust/finalize raised GNATCOLL.VFS.VFS_INVALID_FILE_ERROR: gnatcoll-vfs.adb:340), but in the end I managed to get it up and running.

Edit2: After playing around with it, I'm extremely impressed with what spark can do. I made a function to add 7 to numbers. Tried putting a post condition that the return value is bigger than input. "Nuh uh, it could overflow". Ok so I add a pre condition that numbers must be less than 100. "Uhm, buddy you are passing in 200 right there". This is useful stuff for real and easy to write too.

[ Parent | on HN ]

Re:I can’t believe that I can prove that it can sort by yannickmoy on Monday July 04, 2022 @02:12PM (#31980152)

you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html

It also explains how to install GNATprove: ``alr with gnatprove``

[ Parent | on HN ]

Re:I can’t believe that I can prove that it can sort by im3w1l on Monday July 04, 2022 @02:37PM (#31980402)

Sorry if it was confusing I kind of jumped between the issues I had with various approaches. I did manage to get gnatprove through alire through just that command, it was the apt gnat that didnt have gnatprove. What I wasn't sure how to correctly do with the alire install was

  cd ~/.emacs.d/elpa/ada-mode-i.j.k
  ./build.sh
  ./install.sh

Actually I didn't get that working with any of the options I tried I guess.

[ Parent | on HN ]

Re:I can’t believe that I can prove that it can sort by layer8 on Monday July 04, 2022 @12:38PM (#31978990)

I predict that one day it will be common for this to be a builtin language feature.

[ Parent | on HN ]