Ori Bernstein

As the developer of Myrddin (http://eigenstate.org/myrddin.html), I felt the need to fill it in for my pet language:

You appear to be advocating a new:
[ ] functional [ ] imperative [ ] object-oriented [x] procedural
[ ] stack-based [x] "multi-paradigm" [ ] lazy [x] eager
[x] statically-typed [ ] dynamically-typed [ ] pure [x] impure
[ ] non-hygienic [ ] visual [ ] beginner-friendly
[ ] non-programmer-friendly [ ] completely incomprehensible

programming language. Your language will not work. Here is why it
will not work.

You appear to believe that:
[ ] Syntax is what makes programming difficult
[ ] Garbage collection is free
[ ] Computers have infinite memory
[x] Nobody really needs:
[x] concurrency [x] a REPL [x] debugger support [x] IDE support [ ] I/O
[x] to interact with code not written in your language
[ ] The entire world speaks 7-bit ASCII
[x] Scaling up to large software projects will be easy
[x] Convincing programmers to adopt a new language will be easy
[ ] Convincing programmers to adopt a language-specific IDE
will be easy
[ ] Programmers love writing lots of boilerplate
[ ] Specifying behaviors as "undefined" means that programmers
won't rely on them
[ ] "Spooky action at a distance" makes programming more fun

Unfortunately, your language (has/lacks): [Lacks => L, Has => H]
[L] comprehensible syntax [L] semicolons
…

It's not. Like most of academic ones, it can be picked up or clean-slated if people really want it. The authors tend to move on, though, as in BitC (unfortunately...). I have some others for you, though. Most research is on automatically transforming C instead of a safer, manually-done C. Best are these:

https://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/

http://sva.cs.illinois.edu/downloads.html

http://dslab.epfl.ch/proj/cpi/

Paper mentioning several of the safe C's, including those like Vault you can't have:

https://pdfs.semanticscholar.org/a890/a850dc78e65e26f8f4def435b17094ce08cf.pdf

Galois, as usual, graciously open-sourced two of theirs (Ivory & Tower) that's already fielded in real world:

http://ivorylang.org/

Popcorn and TALC are older ones in prototype form:

https://www.cs.cornell.edu/talc/releases.html

Someone here showed me this one I haven't evaluated but is used in compiler front-end:

https://eigenstate.org/myrddin/

The C0 one used in Verisoft is embedded in vc0compiler-trunk probably. They did great things with it but I haven't been brave enough to try to retrieve it ;).

http://www.verisoft.de/VerisoftRepository.html

So, altogether, what remains is quite scattered and prototype form. Plus, you still have to rewrite the software. So, I've mostly been recommending people apply Softbound, SAFECode, and CPI to their code just to see what happens. If it still works and fast enough, then just use it as it covers most bases. Also, contributing to…

some others worth checking out (all largely single-developer efforts):

http://www.ats-lang.org/ [ml + c + everything dialled up to eleven. linear and dependent types. comes out of academia, but under active development and slowly beginning to gather a community.]

https://eigenstate.org/myrddin/ [not really familiar with this one but it looks interetsing. close to the metal, has pattern matching over algebraic datatypes but seems more towards the c than the ml end of the spectrum from the brief glance i took.]

http://mythryl.org/ [never took off, sadly; i really liked the looks of this one and its ambitious goals. strong sml influence, with better posix integration and some c-like surface features. developer is currently battling cancer: http://mythryl.org/pipermail/mythryl/2016-April/000942.html]

http://felix-lang.org/ [spawn of ml + c++ rather than ml + c. under enthusiastic if haphazard development.]

there have been a few others i've seen pop up over the years; i keep meaning to make a website or at least a github awesome-style list cataloguing and tracking them.

I've actually been building a teaching VM with these properties. You can't take the address of arbitrary values (so there's no distinction between lvalues and rvalues), there's no pointer arithmetic (instead you have type-safe primitives for record access and array indexing), all arrays (including strings) know their length and bounds-check accesses, and unions behave more like sum types, always knowing precisely what type they have stored. All these constraints ensure you can never convert a number to an address, or generate an address to an illegal value. More info about the goal and rationale: http://akkartik.name/post/mu; http://github.com/akkartik/mu.

I also recently found out about http://eigenstate.org/myrddin which seems more mature with very similar goals/aesthetics. I've been digging into it a fair bit.

Finally, on the extreme other end of the spectrum, there's Rust.

Being taught this rule in undergrad really hampered my appreciation of C. As I've said in a previous comment, the real key that unlocked understanding C declarations for me is the mantra "declaration follows use." You declare a variable in C in exactly the same way you would use it: if you know how to use a variable, then you know how to read and write a declaration for it. Once I understood this elegant idea, it became hard to enjoy using statically typed languages that eschew it.

It is explained in more detail at this link:
https://eigenstate.org/notes/c-decl