You can take a look at Low* (a subset of F*) that can be compiled to high performance C code. Once you have C code you can use it from Unity/C#. Though I don't immediately see the value of doing that unless you need formal guarantees of something.

I wonder what the experience of using Fiat is like. Does it degenerate to requiring so much specification that there's no interesting variance in the programs that it writes? Maybe that’s a better way to arrive at that program because what you write decomposes by feature rather than by computational step, but I’m still curious what that process is like for a programmer on average. Another question is, if your code is used non-deterministically to write programs, how do you convince yourself that you’re done—that you won’t get some degenerate “return null” implementation next time you compile because you overlooked a hole in your spec? Do you add unit tests? The initial Cache ADT in the paper had that problem; it described a cache algorithm family that contained every cache algorithm including the one that never adds anything to the cache. The authors knew it had that problem, but in general, how do you?

That is my main goal in general. (And seems the holy grail)

@Prathyush you might be interested too.