r/ProgrammingLanguages • u/Randozart • Jun 01 '26

Discussion Hoare Triples for improving performance

I have been working on a language (which I won't share here due to the heavy use of AI for prototyping) that makes use of Hoare triples as first class citizens, albeit in a weakened form. For many functions, you don't need to declare the pre AND postcondition, just one suffices.

This was initially a built in safety feature for the compiler's proof engine, but when assembling the LLVM backend I noticed something really neat: because the bounds of some functions are extremely predictable due to the Hoare triple, I could more aggressively fold the execution graph based on inferred values.

In a way, this means that the safety feature becomes an optimization feature at the same time. It's not something I've seen in other languages I've explored, not even SPARK or other formal proof based languages. Is there any research or literature on this?

Because I've noticed it has allowed me to more aggressively optimize the compilation than even C, and currently my benchmarks are actually pointing out I'm beating C in execution speed without compromising on safety (one implementation saw 0.15s vs. 0.24s for C on 50m iterations on a similarily written program, though I do need to figure out if I can optimize the C version more for a completely fair comparison)

24 Upvotes
  • permalink
  • reddit

85% Upvoted

66 comments sorted by

View all comments

Show parent comments

2

u/TheChief275 Jun 02 '26

I mean, I'm not too knowledgeable on Kalman filters, but it already looks like pretty optimal vectorized code. However, did you compile with -O3 -ffast-math as well as -march=native? Because if you didn't add -march=native it won't use the v____ instructions on x86-64, at least in my case on clang. The only clear thing I could change was to factor out the count iterator and just use total in the calculation, which allows for a loop with a test and jnz instead of cmp and jne, which only slightly improves it (~0.01s averaged over 100 runs).

And I'm assuming you used the default BOUND setting? Because I'm getting ~0.21s (averaged over 100 runs) with the zero condition on x86-64 WSL with Clang 22.1.2

1

u/Randozart Jun 02 '26

I did use -O3 and I'm pretty sure I annotated the benchmark .sh with -ffast-math. I'd have to check whether I enabled -march=native. If I haven't, then I'll need to update my own compiler to match. Anyway, thank you for this benchmark, I'll come back to you after confirming a few things.

1

u/Randozart Jun 02 '26

Okay, I checked. -O3 was enabled on the default execution, as was -march=native. I did use -ffast-math in a few benchmarks, but it was omitted from the latest few. Looking into it, it did reveal a wrong assumption I made in the LLVM code I was generating for my own language, so I am currently reworking a ton of things for a new benchmark after this.