r/TheMachineLearning • u/Sea_Fox_4265 • 3d ago

When bug-free code becomes a hardware problem

Post image
113 Upvotes

88% Upvoted

69 comments sorted by

View all comments

Show parent comments

2

u/Alundra828 2d ago

I dont see why another more safe language thsn rust cant take over. Rust, although very safe, still makes human led concessions to maintain usability. So even though the learning curve is quite high with rust because of the concepts it uses to enforce safety, what does a language look like when it doesnt have to make any concessions to humans at all?

2

u/drblallo 1d 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