Hacker News new | ask | show | jobs
by ufo 1453 days ago
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?
2 comments
im3w1l 1453 days ago
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.

link
yannickmoy 1453 days ago
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``

link
im3w1l 1453 days ago
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.
link
layer8 1453 days ago
I predict that one day it will be common for this to be a builtin language feature.
link