4 ms·
Sireum Logika
- jldugger 3y agoNice seeing work from a former professor of mine on HN. A lot of the faculty at KSU work on formal verification tooling but industry seems to avoid it in most cases (yes, Amazon uses TLA+ sometimes, allegedly). And now I work on AI products where correctness is itself an ambiguous idea. I guess the challenge is that formal verification of an application in some sense depends on the correctness of its dependencies: the OS, the libraries, the compiler, etc. And maybe even hypervisor, silicon, and network switches!
- ashupadhi01 3y agoHey, what kind of work are you currently doing in AI? Just asking out of curiosity. I want to have a brief chat with you about these proof checkers and verification systems. I never got the gist of all these. Stuffs like lean theorem prover. I will be glad If you take out some time.