They are from Microsoft and seem like they are proof assistants? Besides syntactical differences are there practical aspects that make them different from one another (say ability to do automation,...