I’ve been working sporadically on a strict stack-based functional language called Kitten, with the goals of avoiding GC and libc. No plans for dependent types, but you might like to keep an eye on it anyway: https://github.com/evincarofautumn/kitten