Skip to content

Comment on Borrow-checking without type-checkingparent

Comments

You seem to have no idea what you're talking about. Type theory is a thing, much older than any compiler. And soundness has a meaning.

It just means type errors are checked at runtime instead of compile time.

This is a fundamental misconception. A type checker proves the absence of errors. It doesn't check for error conditions. That is: A program that isn't (cannot be proven to be) well-typed can very well be correct. But a program that is well-typed is guaranteed to be free from certain errors.

What you call "dynamically typed", in contrast, is comsequent just value inspection and stopping the evaluation/execution early. A program that has been executed successfully often is not necessarily correct.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.