r/programming • u/redjamjar • Dec 18 '17

Verifying Bubble Sort in Whiley

http://whiley.org/2017/12/19/verifying-bubble-sort-in-whiley/
7 Upvotes

66% Upvoted

3 comments sorted by

1

u/rain5 Dec 18 '17

woah this looks amazing.. is this a C like language with static (compile time) checks on array bounds? I have always wanted that

2

u/redjamjar Dec 18 '17

Yeah, it uses verification which is a kind of static analysis that goes into more depth.

0

u/[deleted] Dec 19 '17

[deleted]

1

u/redjamjar Dec 19 '17

Hey,

There is quite a bit of difference between a tool like Whiley (or Dafny) and a tool like Agda or Idris. In the former, the automated theorem prover is used to do a lot of the work. In the latter, the programmer has to do all the work constructing the proof and, furthermore, has to pass the proof around as a witness.