Name: Anonymous 2018-10-12 17:08
So, why are you not using dependent types yet? Do you like your programs randomly crashing?
doesNotContainUnescapedQuotesthat might be the only way to prevent shell injection but it's an anus-backwards approach when it comes to SQLi. the correct solution is not treating SQL queries as strings. see: parametrized queries.
Buffer overflows are also logic bugs.buffer overflows aren't really what security people would call logic bugs. this term refers to unintended consequences of a program's high-level design, not low-level details about programming language, calling convention and the processor architecture.
Nice memedependent types solve halting problem?
Dependent types can't prevent bugs in other programs.how would they prevent those bugs if an OS was written in a dependently typed language? that's a clear example of what I mean by 'logic bugs'