Thread

1. AnimalMuppet · 1791048809 · focus · HN ↗

   I haven't played with it at all, but the writeup looks promising. Moving a bunch of things into the type system and out of runtime crashes is one of the ways we make progress.

   1. dnautics · 1791055681 · focus · HN ↗

      I think this is wrong. Type systems should be simpler, and you should design it so that your language is easily and correctly statically checked. Not all invariants necessarily have to be verified at the same cadence (compile time)

      1. treyd · 1791056182 · focus · HN ↗

         > you should design it so that your language is easily and correctly statically checked.

         You do that by making the type system more sophisticated.

         If you have a really important invariant that you really don't want to be violated due to run-time behavior/input, it's a huge benefit to have a compiler that can statically check that it actually can't be. That's one of the main benefits of having type systems, not just describing the shape of data structures in memory.

         1. dnautics · 1791056698 · focus · HN ↗

            You can perform static analysis outside of the compiler without putting things in the type system?

            C is a bad language to do this with for various reasons, but as a simple example:

                char* buf = malloc(SIZE);
                free(buf);
                free(buf);
            

            There is absolutely no reason why static analysis should not be able to see what the problem is here.

            1. 0xdeafbeef · 1791061520 · focus · HN ↗

               uintptr_t x = opaque((uintptr_t)p); free((void *)x); free(p);

               How will you find such violations if opaque comes from so or some ffi, so compiler can't see through? you can't. It's heuristics. Sound type system is much stronger

               1. dnautics · 1791087459 · focus · HN ↗

                  *ffi

                  Christ. Even rust makes ffi unsafe.

                  I mean you can annotate it if you want. Just tell the analyzer in a separate file, get the variable at this line on this file has these guarantees.

                  You could even annotate dependencies that didn't use your static analyzer. You could track custom invariants that your language designer didn't put in the type system.

                  1. treyd · 1791090263 · focus · HN ↗

                     > Even rust makes ffi unsafe.

                     Which is why every library that wraps C APIs provides safe wrappers that express the implicit expectations within Rust's type system. Yes the low-level calls are unsafe, of course they are, but then we expose them with a safe interface that consumers actually use.

Unofficial Hacker News client; not affiliated with Y Combinator.