It will prove the bugs were corrected implemented... :-) And that your mistaken specification of the tax rules in Switzerland, was correctly translated to code, and that your mistaken specification of the process to request a mortgage is mathematically valid...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic...
I was picking mostly on the rust religion at first. But then I looked things up and ran into <a href="https://en.wikipedia.org/wiki/Rice%27s_theorem" rel="nofollow">https://en.wikipedia.org/wiki/Rice%27s_theorem …
I wouldn't say it's all rubbish - it's very easy for someone new to theorem proving to presume the equivalent of "strong typing will eliminate the possibility of errors", but the more correct understanding is "strong typing will reduce the number of things you have to keep in your head at any one time thus reducing the possibility of errors".
The thing with ubuntu's rust coreutils is that they, for example, crash when told to recurse because they use actual recursive calls to go into subdirs and run out of stack space if the structure is big enough.
any of the quite many cost-aware logical frameworks. it’s SO. easy. to. do. you fools are just willfully ignorant on how to represent reasoning, despite alleging yourselves to be computer scientists?
nottorp · · focus · HN ↗
Betelbuddy · · focus · HN ↗
Jesus, I cant stand formal methods people...
nottorp · · focus · HN ↗
cmrx64 · · focus · HN ↗
it’s all rubbish, grandparent is a small mind who can’t figure out how it’s a step up from nothing.
svieira · · focus · HN ↗
nottorp · · focus · HN ↗
What formal correctness proof will detect that?
cmrx64 · · focus · HN ↗