|11 days ago||4 days ago|
|Standard ML||Standard ML|
|BSD 3-clause "New" or "Revised" License||GNU General Public License v3.0 or later|
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
There's an ongoing effort to rewrite Principia Mathematica using Coq
5 projects | reddit.com/r/math | 3 Dec 2021
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.
Is there a formally-proven real-time language/computing env. or operating system?
2 projects | reddit.com/r/ProgrammingLanguages | 7 Sep 2022
There is also Cake ML which is a formally verified functional programming language compiler and runtime.
CakeML: A Verified Implementation of ML
2 projects | reddit.com/r/sml | 7 Mar 2022
There is also a CakeML -> Standard ML compiler though it seems to have been built to translate benchmarks and sort of old so I'm not sure how comprehensive it is: https://github.com/CakeML/cakeml/tree/master/unverified/front-end2 projects | reddit.com/r/sml | 7 Mar 2022
3 projects | news.ycombinator.com | 15 Jan 2022
> One guess is that lisps cope with being minimal through use of macros and metaprogramming, it's difficult for a typed language to support that level of metaprogramming while maintaining the various guarantees that one wants from such a system.
Difficult, but certainly not impossible .
Two Mechanisations of WebAssembly 1.0
2 projects | reddit.com/r/ProgrammingLanguages | 3 Jan 2022
If this interests you, I'd highly recommend checking out CompCert (docs here) and CakeML.
Please critique Pancake, my first ever langdev project!
3 projects | reddit.com/r/ProgrammingLanguages | 11 Oct 2021
A Proven Correct C Compiler (Used by Airbus)
7 projects | news.ycombinator.com | 26 Jun 2021
CakeML is another formally verified compiler. Notably, unlike compcert, it is open source.
The language it implements (an sml dialect) is high-level and garbage collected, meaning that it is not usable in all of the same domains, but work is ongoing to reuse much of the compiler infrastructure for 'pancake', a low-level language.
What are some alternatives?
NyuziProcessor - GPGPU microprocessor architecture
koika - A core language for rule-based hardware design 🦑
smlpkg - Generic package manager for Standard ML libraries and programs
Daikon - Dynamic detection of likely invariants
CompCert - The CompCert formally-verified C compiler
pancake - stack-oriented pain-maximising toy programming language