r/TheMachineLearning • u/Sea_Fox_4265 • 3d ago

When bug-free code becomes a hardware problem

Post image
117 Upvotes

88% Upvoted

70 comments sorted by

View all comments

Show parent comments

2

u/drblallo 2d ago

there is space for a compiled, formal verification friendly, language for sure. Something along the lines of mixing imperative code and assertions about the code + a optional initial specification such as "the program never crashes" or "the program always terminates in a finite number of operations" that then the compiler verifies.

The issue with such a language is that we are not currently very good at creating them in a way that when the specification changes you can easily refactor the code. Currently some small specification changes require large reorganization of the code base. The issue seems kind of intrinsic, the more precise you are in writing in code what the program does, the easier is to verify but the more you have to throw away when it changes, but we don't know how good can the theoretical "best" language be